CAIN-42 formal models, checked with TLC (the TLA+ model checker), 2026-09-27.

CAINPBFTCommitSafety.tla      PBFT commit and view-change rules: N=4, f<=1, Q=3, one sequence, views 0-1, values X/Y.
  Invariants: Agreement (no two honest replicas execute different values), CommitOnlyWhenPrepared.
  Configurations: Byzantine replica (290,806 distinct states), Byzantine view-0 leader (670,340), none (4,198,642): no violation.
  Mutants that MUST fail: the pre-fix "execute on a prepared certificate" rule, and a new primary that ignores
  reported certificates: both violate Agreement.

CAINMCPGateAuthorization.tla  MCPGate consensus-authorization gate: an attacker presents any body with any call.
  Invariants: NoExecWithoutQuorum, ActionBinding, IdentityBinding, ContextBinding, NotExpired, SingleUse.
  Configurations: Byzantine member (553,996 distinct states), none (1,591,308): no violation.
  Mutants that MUST fail: quorum threshold 2, and each gate check removed in turn: each violates exactly the
  invariant that check protects.

Each *.tlc.json lists every run with the numbers TLC printed, and the spec's SHA-256.

Reproduce (Java 11+, tla2tools.jar from https://github.com/tlaplus/tlaplus/releases). The models are published as
*.tla.txt; save them as *.tla:
  BASE=https://clawx.click/evidence/formal-2026-09-27   # or https://cainstudio.online/proof/bundle/formal-2026-09-27
  for m in CAINPBFTCommitSafety CAINMCPGateAuthorization; do curl -so $m.tla "$BASE/$m.tla.txt"; done
  printf 'CONSTANTS\n  Byz = {"n4"}\n  OldRule = FALSE\n  IgnoreReports = FALSE\nSPECIFICATION Spec\nINVARIANTS\n  TypeOK\n  Agreement\n  CommitOnlyWhenPrepared\n' > CAINPBFTCommitSafety.cfg
  java -cp tla2tools.jar tlc2.TLC -deadlock -config CAINPBFTCommitSafety.cfg CAINPBFTCommitSafety.tla
  (set OldRule = TRUE or IgnoreReports = TRUE to see the counterexample)
  printf 'CONSTANTS\n  Byz = {"n4"}\n  Thresh = 3\n  SkipExpiry = FALSE\n  SkipAction = FALSE\n  SkipIdentity = FALSE\n  SkipContext = FALSE\n  SkipReplay = FALSE\nSPECIFICATION Spec\nINVARIANTS\n  TypeOK\n  NoExecWithoutQuorum\n  ActionBinding\n  IdentityBinding\n  ContextBinding\n  NotExpired\n  SingleUse\n' > CAINMCPGateAuthorization.cfg
  java -cp tla2tools.jar tlc2.TLC -deadlock -config CAINMCPGateAuthorization.cfg CAINMCPGateAuthorization.tla
  -deadlock turns off deadlock detection: the models are bounded, so behaviours end in terminal states; only safety is checked.

Not claimed: a proof about the Python implementation; unbounded parameters (more replicas, sequences, views);
liveness; a machine-checked proof (these are exhaustive model checks within the bounds above).