Surface: fv · Severity: low (coverage boundary of the F3 fix; the strong form is refuted) · Evidence: PoC (two canary variants in an 8.2 GB scratch copy) · Target: f91aa82
Claimed (map row 3, 2026-07-23): "the default closure check also accepts an arbitrary new project axiom."
Verified today: the strong form is REFUTED — a False axiom consumed by an advertised theorem is rejected with all four polluted headlines named. The weak form holds: adding axiom unmodeled_assumption_canary : False + theorem canary_one_eq_two : 1 = 2 := … in a new module imported from Extracted.lean keeps lake build green AND the closure gate green (the canary appears 0 times in the dump) — nothing polices project-wide axiom introduction for non-dumped theorems. The shipped axiom Evil : False negative control is correctly quarantined (not root-imported, never built).
Fix (cheap): a project-wide axiom census lint for extracted/ — every ^axiom declaration must be in the disclosed set {keccak256_pure, sha256_pure_bytes, hmac_sha512_pure_bytes, quarantined NegativeControl.Evil}. Today that grep returns exactly those four, so the gate starts green. Found 2026-08-20 FV red-team.
Surface: fv · Severity: low (coverage boundary of the F3 fix; the strong form is refuted) · Evidence: PoC (two canary variants in an 8.2 GB scratch copy) · Target: f91aa82
Claimed (map row 3, 2026-07-23): "the default closure check also accepts an arbitrary new project axiom."
Verified today: the strong form is REFUTED — a
Falseaxiom consumed by an advertised theorem is rejected with all four polluted headlines named. The weak form holds: addingaxiom unmodeled_assumption_canary : False+theorem canary_one_eq_two : 1 = 2 := …in a new module imported fromExtracted.leankeepslake buildgreen AND the closure gate green (the canary appears 0 times in the dump) — nothing polices project-wide axiom introduction for non-dumped theorems. The shippedaxiom Evil : Falsenegative control is correctly quarantined (not root-imported, never built).Fix (cheap): a project-wide axiom census lint for
extracted/— every^axiomdeclaration must be in the disclosed set {keccak256_pure,sha256_pure_bytes,hmac_sha512_pure_bytes, quarantinedNegativeControl.Evil}. Today that grep returns exactly those four, so the gate starts green. Found 2026-08-20 FV red-team.