The formal gates printed FAILED and exited 0

docs/papers/amendment-2c-c2-verification-substrate.md

@@ -1168,7 +1168,17 @@ named storage-substrate exception.
 **Formal-model coverage — DISCHARGED under the stated symbolic assumptions (ruling G).**
 `lean4/DSMEconomicSmtSeparation.lean` carries obligations 1–7; `tla/DSM_EconRegisterObservation.tla`
 carries the concurrent register-observation half, with five deliberate-falsification configs that
-are machine-gated on the invariant each must violate. This is coverage of the normative **models**,
+are classified on the invariant each must violate.
+
+> **Correction, recorded after the fact.** This sentence originally read *"machine-gated"*. The
+> classification was real — `run_all` normalizes every verdict and inverts the expected-to-fail
+> configs correctly — but **CI could not act on it**: `tla-check` printed `FAILED specs: …` and
+> returned `Ok`, and neither `main` nor the CI step converted that into a non-zero exit. A violated
+> invariant, a falsification config that stopped falsifying, and a spec silently dropped from the
+> registry were all green. The same defect affected `property-tests` and `implementation-traces`.
+> The gate became load-bearing only with the corrective change that added exit-status enforcement
+> and a registry-count tripwire; until then, "machine-gated" was true of the runner's bookkeeping
+> and false of CI. This is coverage of the normative **models**,
 not a refinement proof from the Rust — see the claim boundary in ruling G.
 
 **Conformance surface — OWED.** Rev 15 has no conformance row for the economic register, `R_econ`,

tools/vertical_validation/src/main.rs

@@ -180,11 +180,11 @@ async fn main() -> anyhow::Result<()> {
         }
 
         Commands::PropertyTests { iterations, seed } => {
-            run_property_tests(iterations, seed);
+            run_property_tests(iterations, seed)?;
         }
 
         Commands::ImplementationTraces => {
-            run_implementation_traces();
+            run_implementation_traces()?;
         }
 
         Commands::Adversarial => {
@@ -223,6 +223,26 @@ async fn main() -> anyhow::Result<()> {
     Ok(())
 }
 
+/// Turn an aggregate verdict into a process exit status.
+///
+/// A gate that PRINTS "FAILED" and then exits 0 is not a gate. CI reads the
+/// process status, not the report text, so a suite that summarises its own
+/// failures and returns `Ok` is indistinguishable from a green one to the only
+/// consumer that matters.
+///
+/// Enforcement runs AFTER the report is printed, so the failing spec, property
+/// or trace — and the invariant it violated — stay visible in the log.
+fn enforce(gate: &str, total: usize, failing: &[String]) -> anyhow::Result<()> {
+    if failing.is_empty() {
+        return Ok(());
+    }
+    anyhow::bail!(
+        "{gate}: {} of {total} FAILED — {}",
+        failing.len(),
+        failing.join(", ")
+    )
+}
+
 /// Collect TLAPS proof results (progress on stderr, no report printed).
 async fn collect_proof_results(
     root: &std::path::Path,
@@ -341,6 +361,18 @@ async fn run_tla_check(
     };
 
     print!("{}", report.render_ascii());
+
+    // A violated invariant, or a falsification config that failed to falsify,
+    // must redden CI. `run_all` has already NORMALISED every verdict, including
+    // inverting the expected-to-fail configs, so `passed` here is the gate's
+    // answer and not TLC's raw one.
+    let failing: Vec<String> = results
+        .iter()
+        .filter(|(_, r)| !r.passed)
+        .map(|(s, _)| s.label.clone())
+        .collect();
+    enforce("TLA+ model checking", results.len(), &failing)?;
+
     Ok(results)
 }
 
@@ -368,8 +400,15 @@ async fn run_benchmark(
 }
 
 /// Run property tests standalone.
-fn run_property_tests(iterations: u64, seed: u64) {
+fn run_property_tests(iterations: u64, seed: u64) -> anyhow::Result<()> {
     let results = property_tests::collect_property_test_results(seed, iterations);
+    let total = results.results.len();
+    let failing: Vec<String> = results
+        .results
+        .iter()
+        .filter(|r| !r.passed)
+        .map(|r| r.property_name.clone())
+        .collect();
     let report = VerticalValidationReport {
         proof_results: Vec::new(),
         tla_results: Vec::new(),
@@ -381,11 +420,19 @@ fn run_property_tests(iterations: u64, seed: u64) {
         bilateral_throughput_results: None,
     };
     print!("{}", report.render_ascii());
+    enforce("Real-code bridge properties", total, &failing)
 }
 
 /// Run deterministic implementation traces standalone.
-fn run_implementation_traces() {
+fn run_implementation_traces() -> anyhow::Result<()> {
     let results = implementation_traces::collect_implementation_trace_results();
+    let total = results.results.len();
+    let failing: Vec<String> = results
+        .results
+        .iter()
+        .filter(|r| !r.passed)
+        .map(|r| r.trace_name.clone())
+        .collect();
     let report = VerticalValidationReport {
         proof_results: Vec::new(),
         tla_results: Vec::new(),
@@ -397,6 +444,7 @@ fn run_implementation_traces() {
         bilateral_throughput_results: None,
     };
     print!("{}", report.render_ascii());
+    enforce("Implementation traces", total, &failing)
 }
 
 /// Run adversarial tests standalone.

tools/vertical_validation/src/tla_runner.rs

@@ -23,6 +23,16 @@ use crate::tla_trace_replay::{
 };
 
 /// Configuration for a single TLA+ model check run.
+/// How many specs `standard_specs()` must register.
+///
+/// The registry is Rust, not a glob, so a spec deleted from `standard_specs`
+/// leaves nothing behind for a file count to notice — the suite simply gets
+/// smaller and stays green. This is the analogue of the Lean gate's
+/// `expected=12` module count in CI, and it exists for the same reason: an
+/// anti-skip tripwire is cheap, and a silently shrinking formal suite is the
+/// failure mode that looks most like success.
+pub const EXPECTED_STANDARD_SPECS: usize = 13;
+
 #[derive(Debug, Clone, Serialize)]
 pub struct TlaSpec {
     /// Human-readable label (e.g., "DSM_tiny")
@@ -592,6 +602,14 @@ impl TlaRunner {
         include_liveness: bool,
     ) -> anyhow::Result<Vec<(TlaSpec, TlcResult)>> {
         let mut specs = Self::standard_specs();
+        if specs.len() != EXPECTED_STANDARD_SPECS {
+            anyhow::bail!(
+                "standard_specs() registers {} specs, expected {EXPECTED_STANDARD_SPECS}. \
+                 A spec was added or removed. Update EXPECTED_STANDARD_SPECS deliberately, \
+                 so that dropping a spec from the registry cannot leave this gate green.",
+                specs.len()
+            );
+        }
         if include_liveness {
             specs.extend(Self::extended_specs());
         }
@@ -644,6 +662,43 @@ impl TlaRunner {
     }
 }
 
+#[cfg(test)]
+mod registry_tests {
+    use super::*;
+
+    /// The registry is the suite. `run_all` bails on a mismatch so CI cannot go
+    /// green on a shrunken suite, and this test fails the same way in
+    /// `cargo test` — before anyone waits on TLC — so the count is corrected
+    /// deliberately rather than discovered in a model-checking log.
+    #[test]
+    fn the_standard_spec_registry_is_the_expected_size() {
+        assert_eq!(
+            TlaRunner::standard_specs().len(),
+            EXPECTED_STANDARD_SPECS,
+            "standard_specs() changed size. Update EXPECTED_STANDARD_SPECS on purpose."
+        );
+    }
+
+    /// Every falsification config must name an invariant the spec actually
+    /// declares. A typo here degrades silently into "a different failure",
+    /// which reads as a real defect in the model rather than in the registry.
+    #[test]
+    fn every_falsification_config_names_an_invariant_its_spec_declares() {
+        for spec in TlaRunner::standard_specs() {
+            let Some(expected) = spec.expect_violation.as_deref() else {
+                continue;
+            };
+            assert!(
+                spec.invariants.iter().any(|i| i == expected),
+                "{} expects a violation of `{expected}`, which is not in its own \
+                 declared invariants {:?}",
+                spec.label,
+                spec.invariants
+            );
+        }
+    }
+}
+
 fn dfid_depth_for_config(config_text: &str) -> u64 {
     let Some(re) = Regex::new(r"(?m)^\s*(MaxStep|MaxChain)\s*=\s*(\d+)\b").ok() else {
         return 10;