PiProof v0.16.1 — Mechanized Verification Goes Live

PiProof v0.16.1 — Mechanized Verification Goes Live

The TLA+ model is no longer hand-checked. TLC now runs on every push and
PR, and CI fails unless it reports "Model checking completed. No error
has been found."

What shipped

• CI job formal-tlc: Temurin 21 via pinned actions/setup-java SHA +
  tla2tools.jar v1.7.4 verified against the official release SHA1
  (bee4a54f3ee3d4afc347c3240ec2d9e93b075104) before use.
• Verified result: the complete state space — 122 distinct states — with
  TypeOK, AtMostOneAccept (INV-04), AcceptImpliesBurn, and
  BurnOnlyOnPass (INV-05) all holding.

The first machine run earned its keep immediately

Two real modeling flaws, caught by TLC before any human reviewer:

1. EXTENDS Naturals → Integers — unary minus (the rejection-code
   encoding) is not defined in pure Naturals.
2. The G8 environment choice was separable from its consequence; a verifier
   could read a snapshot before the environment committed, producing a stuck
   path that TLC's deadlock analysis exposed. G8's choice and outcome are
   now one atomic action, and clean termination is an explicit
   TerminalStutter action — preserving deadlock detection for genuinely
   stuck mid-pipeline states rather than disabling it with -deadlock.

Maturity movement

Row #14 (mechanized verification): drafted → partially held. The
stateful core of G1–G9 is machine-checked continuously; extending coverage
toward the full INV-01…12 set remains open work.

v1.0 remains gated on external review. Details:
CHANGELOG ·
formal/README.md ·
docs/MATURITY.md