This repository is a formal verification suite for Clawdbot, a Discord bot, using TLA+ and the TLC model checker. It provides machine-checkable security models that act as a regression suite: 'green' models should pass (no invariant violation) and 'red' models are deliberately buggy variants that should fail with a counterexample trace. The repo includes over 100 TLA+ specifications covering gateway exposure, node command policy, pairing store invariants, routing isolation, Discord-specific conformance (role gating, PluralKit, thread binding), and liveness properties. It also contains scripts to extract tool group definitions from the main Clawdbot codebase and generate TLA+ configuration constants, ensuring conformance between the formal models and the implementation. The architecture is a collection of TLA+ specs and model configs orchestrated by a Makefile, with a vendored TLC jar and a CI pipeline that runs selected models on each PR. While the models are domain-specific to Clawdbot, the patterns (e.g., policy precedence, pairing store with expiry and cap, tokenized approvals) are reusable templates for formal verification of similar systems.