The formal gates printed FAILED and exited 0

[cryptskii]

CI reads the process status, not the report text. All three dsm_vertical_validation steps summarized their own failures and returned Ok, so a violated invariant, a falsification config that stopped falsifying, a failed bridge property and a failed implementation trace were every one of them green.

Found while surveying the Rust surface for 2c-C3 Phase D. Split out as infrastructure debt rather than folded into C3, because it predates C3 and C3 adds no TLA+ specs.

What was verified before anything changed

collect_tla_results computes all_passed, prints FAILED specs: …, and returns Ok(results) unconditionally. run_tla_check returns Ok(results). main does run_tla_check(...).await? and falls through to Ok(()). main.rs has no process::exit, no ExitCode and no bail! on a verdict anywhere. The CI step is a bare cargo run … -- tla-check with no grep on the log.

run_property_tests and run_implementation_traces return () — collect, render, return, no failure check at all.

So the only things that could redden those three jobs were a missing java, a missing .tla/.cfg, or a build failure.

What was already correct

The expected-violation semantics were fully implemented. run_all already normalizes every verdict and inverts the falsification configs: expected invariant violated is a pass, no violation is "the invariant is decoration", a different violation is "a different failure". None of that changes here.

The defect was never the classification. It was that nothing turned the aggregate into an exit status.

The change

• enforce(gate, total, failing) bails with the failing labels, called after the report prints so the failing spec and its invariant stay visible.
• All three commands route through it; two of them now return Result.
• EXPECTED_STANDARD_SPECS = 13, asserted in run_all. The TLA registry is Rust, not a glob, so a spec deleted from standard_specs leaves nothing for a file count to notice — the suite just gets smaller and stays green. The Lean gate has expected=12 in CI; TLA+ had no counterpart.
• Two unit tests: registry size, and that every falsification config names an invariant its own spec declares (a typo there degrades silently into "a different failure", which reads as a defect in the model rather than in the registry).

Mutation controls — all executed, all restored

#	mutation	result
A	ordinary spec pointed at a falsifying config	exit 1 — FAILED specs: EconRegisterObservation
B	falsification config neutered so nothing violates	exit 1 — "must violate EmptinessIsGrounded, but saw no violation at all — the invariant is decoration"
C	falsification config names the wrong invariant	exit 1 — "saw a different failure: ConflictUnreachable"
D	unmutated suite	exit 0 — All 13 specs PASSED
E	one spec dropped from the registry	exit 1 — registers 12 specs, expected 13
F	one bridge property forced to fail	exit 1 — 1 of 7 FAILED — hash_chain_continuity
G	one implementation trace forced to fail	exit 1 — 1 of 16 FAILED — state_machine_transfer_chain

The baseline suite is genuinely green, so this does not paper over a red spec — it makes 13 specs, 7 properties and 16 traces load-bearing for the first time.

Record correction

Amendment 2c-C2 (merged as #785) said the five falsification configs "are machine-gated on the invariant each must violate." That was true of the runner's bookkeeping and false of CI. The sentence now reads "classified", with a recorded correction naming the exit-status defect and this fix. The classification it describes was real; the enforcement was not.

Verification

make lint exit 0 on the pinned 1.98.0 toolchain; cargo fmt --check clean; clippy --all-targets clean; the 2 new unit tests pass; tla-check exits 0 on the clean 13-spec suite.