Temporal operators (always, eventually, leads_to) and fairness declarations parse and type-check but are not evaluated — the checker is safety-only and reports them as ignored (a warning; the OK verdict now says "safety invariants only"). Implement liveness checking: cycle detection over the state graph for eventually/leads_to under weak/strong fairness. This is the largest remaining capability gap. Tracked in docs/src/tips/roadmap.md.
Temporal operators (
always,eventually,leads_to) and fairness declarations parse and type-check but are not evaluated — the checker is safety-only and reports them as ignored (a warning; the OK verdict now says "safety invariants only"). Implement liveness checking: cycle detection over the state graph foreventually/leads_tounder weak/strong fairness. This is the largest remaining capability gap. Tracked in docs/src/tips/roadmap.md.