# Formal results summary

TLC (TLA+ model checker), 2026-09-27. Models are abstract and bounded; **no proof of the Python implementation and no proved refinement**.

| Model | Run | Distinct states | Generated states |
|---|---|---|---|
| CAINPBFTCommitSafety | Byzantine replica n4 | 290,806 | 1,099,897 |
| CAINPBFTCommitSafety | Byzantine leader n1 | 670,340 | 2,512,355 |
| CAINPBFTCommitSafety | none | 4,198,642 | 18,600,059 |
| CAINMCPGateAuthorization | Byzantine member n4 | 553,996 | 4,048,953 |
| CAINMCPGateAuthorization | none | 1,591,308 | 12,916,185 |
| **Sum (distinct)** | | **7,305,092** | 39,177,449 |

7.3M is a rounded label for the **SUM of distinct states across five configurations**, not one model. Eight deliberately-broken mutants must each violate their invariant (2 PBFT + 6 MCPGate); if a mutant passes, the run is not evidence.

Links: models and raw output at /proof/bundle/formal-2026-09-27/ (CAINPBFTCommitSafety.tla.txt, CAINMCPGateAuthorization.tla.txt, *.tlc.json, REPRODUCE.txt).