Formal Verification (Security Models) - OpenClaw

Goal (north star): provide a machine-checked argument that OpenClaw enforces its intended security policy (authorization, session isolation, tool gating, and misconfiguration safety), under explicit assumptions. What this is (today): an executable, attacker-driven security regression suite:

Each claim has a runnable model-check over a finite state space.
Many claims have a paired negative model that produces a counterexample trace for a realistic bug class.

What this is not (yet): a proof that “OpenClaw is secure in all respects” or that the full TypeScript implementation is correct.