This is the live tool, not a slideshow. Edit a real CMMC control expressed as a temporal specification, run it through the actual TLC model checker on our on-prem box, and ask the on-prem assistant anything. Every verdict below is real output you can falsify.
Walk into the assessment with proof, not hope.
The obligation terminated ~> revoked (every terminated user is eventually revoked) is a liveness property. How robust must the revocation worker be to keep it? Pick a fairness level and run the real checker.
Most 800-171 controls are static predicates. The temporal, process-shaped ones — deprovisioning, onboarding order, recert cadence, ConMon — silently rot in ways no snapshot catches. Those we model-check with TLC. The verdict above is one of them.
The assistant is Llama-3.1-8B (Meta, US-origin) running entirely on your box. No data leaves the host; it runs identically unplugged. Swappable in one line to any model your policy requires. TLC — not the model — is the authority.
Every verdict re-runs from an executable check you can falsify. Edit the spec, change the fairness, and the checker re-computes. Nothing here is baked.
Not a textbox — CodeMirror with TLA+ syntax and Vim / Emacs / VS Code keybindings. Select any expression, press ⇧⌘E, and the on-prem model explains it while you edit.
Author and check specifications across the whole assessment — not one control, all of them — at the pace of a real audit, with the operationalize-every-control pipeline.
Grounded on your SSP, POA&M, and policies; synthetic scenarios sampled from your invariant-satisfying state space; continuous validation wired to your evidence.
Per-control: source → objective → plain meaning → why it's legally hard → checkable rule → verified TLA+ where temporal. Export the proof.