Check safety invariants over every reachable state. Returns a verdict per invariant, with a SHORTEST counterexample trace where one fails.

Check that EVERY reachable state can still reach the goal (AG-EF). Stronger than "the goal is reachable": it catches a state you can enter and never leave.

The spec format, with a worked example.

Schema check with a message naming the offending key.

Render the spec as a Mermaid state diagram, with any counterexample highlighted. An agent that has just been handed a counterexample as a list of dicts can pass this straight back to the user as a picture. Refuses on a graph too large to read rather than returning an unusable blob.