These are standard model-checking capabilities present in other checkers (TLC, SPIN, PRISM/Storm, nuXmv) that musil does not yet have. They are core-verification gaps, complementary to the adoption-ergonomics list in #1. Ranked by value-to-effort. All are pure post-hoc/graph algorithms that fit the dependency-free, explicit-state design. ## 1. Coverage & vacuity reporting (cheapest, highest signal) A green `check` can be meaningless and today there is no way to tell: - an invariant whose antecedent is never reached is **vacuously true** (passes for the wrong reason); - an action that is **never enabled in any reachable state** is dead — usually a guard bug that silently removes behaviour the author believed was covered; - a guard that is **always false** (or always true) quietly changes the model from what was intended. Today: `metrics.py` reports size/branching only; `check` returns `OK` with no coverage view. TLC has action/property coverage; several checkers report vacuity. Proposal: a `coverage(model)` (or a flag on `check`) that, over the already-enumerated reachable graph, returns: actions never enabled (dead) and actions always enabled; invariants that were never "exercised"; and the terminal states. Minimal first cut that needs no new modelling: dead-action detection + an "invariant never had a chance to fail" report (e.g. the invariant returned the same constant across every reachable state). Soundness: none at risk — it is analysis over the graph `check` already builds. ## 2. General (bounded) temporal properties — an LTL layer Today `check_liveness` offers three fixed forms — `<>P` (eventually), `[]<>P` (`everywhere`), and `Q ~> P` (`leadsto_from`) — plus weak/strong fairness. There is no way to state an arbitrary temporal property: `U` (until), `X` (next), `R` (release), `W` (weak until), nested combinations, or safety-LTL such as `[](p -> X q)`. SPIN and TLC take a full temporal formula. Proposal: a small formula AST (`Not/And/Or/Next/Until/Always/Eventually/Release`) checked over the reachable graph via the standard automata-theoretic route (product with a Büchi automaton) or, for these bounded models, a nested-DFS / SCC search reusing the existing lasso machinery. The current fixed forms become sugar over it; fairness composes as a premise (`fair -> property`). Dependency-free. ## 3. Probabilistic / quantitative checking (DTMC / MDP) — exact, not sampled `sim.py` runs seeded **Monte-Carlo** with loss/duplicate probabilities — that is sampling, not verification. There is no way to ask exact quantitative questions: `P(eventually bad) <= 0.01`, expected steps/cost to a goal, or (with both nondeterminism and probability, an MDP) the min/max of those over all schedulers. PRISM/Storm are built for exactly this, and it is the property class that stochastic systems need — nothing in musil currently addresses it. Proposal: let actions carry a probability weight (a probabilistic `Model` variant), build the transition matrix over the reachable graph, and compute reachability probability and expected reward by iterative linear solve / value iteration; MDP variant does min/max value iteration over schedulers. Pure-Python iteration keeps it dependency-free (numpy optional). Larger effort than 1–2; flagged as such. ## 4. Memory-bounded approximate search (bitstate / hash-compaction) — lower priority `check` holds the full `seen` set in memory, so the reachable space must fit in RAM. SPIN's supertrace/bitstate mode stores state hashes instead of full states, trading a small, quantifiable miss probability for verifying far larger spaces. Proposal: `check(..., bitstate=True, hash_bits=...)` storing hashes with a reported collision/coverage estimate. Approximate by construction — must be clearly labelled as such (a passing bitstate run is evidence, not proof). --- Deliberately excluded: partial-order reduction (`REDUCTION_NOTES.md` records why it is deferred) and the adoption-ergonomics items already tracked in #1. Split into per-feature issues as they get picked up.