Ask
Make axiom auditing a first-class, default-on gate in the Lean rules, so a proof target cannot silently depend on sorryAx or an unexpected axiom. Today this is a discipline that each repo re-implements by hand (ordeal checks it manually in lean/Sound.lean; gale's honesty ledger records that Lean proofs are "local only, no CI record"). As a Bazel rule it becomes automatic for every consumer.
Why this is the highest-value check for Lean specifically
Lean's kernel already computes the answer — #print axioms foo returns exactly the axioms a theorem transitively depends on. The vacuity failure it catches is total: a theorem that depends on sorryAx is not proved at all, yet lake build is green and the file looks finished. This is the cheapest possible instance of "the proof did not depend on what you think it did".
Proposed rule features
lean_proof_test / an attribute on the existing test rule — axiom allowlist.
Per-target allowed_axioms = ["propext", "Classical.choice", "Quot.sound"] (the standard classical trio), defaulting to exactly that set. The rule runs #print axioms over the declared theorems and fails the build if any other axiom appears — sorryAx above all. Emit the offending declaration and its axiom set in the failure message.- Fail on
sorry syntactically as well as semantically. A sorry in a definition used by a proof, or in an unexported lemma, may not surface in the top-level theorem's axiom set. Cheap complementary grep-level check, opt-out per target.
- Machine-readable output. Write the per-theorem axiom set to a JSON output (e.g.
<target>.axioms.json) so downstream tooling (rivet evidence, an honesty ledger, a claim-check predicate) can consume "what does this proof actually rest on" as evidence, not prose. This is the piece that makes the gate composable across the org.
- Unused-hypothesis reporting (stretch). The Lean analogue of Dafny's
--warn-redundant-assumptions: a hypothesis in scope that no proof goal required is a signal the theorem is weaker than its statement suggests. Report, don't fail.
Notes
- Items 1–3 are cheap and mechanical; item 4 is the genuinely useful-but-fuzzier one and should be advisory only.
- Precedent for the exact allowlist: ordeal's checker asserts
sorry-free and axiom-clean against {propext, Classical.choice, Quot.sound} — this rule would make that the default posture rather than a per-repo achievement.
- Recommended default: fail closed (unknown axiom ⇒ red). An escape hatch (
allowed_axioms = [...]) keeps it honest by forcing the exception to be written down in the BUILD file, where review sees it.
Background: the research this comes from
A survey of vacuity/adequacy checking (state of the art, primary sources) produced one framing worth internalising, from Kupferman's Sanity Checks in Formal Verification (CONCUR'06): coverage and vacuity are the same check applied to opposite operands — coverage mutates the system, vacuity mutates the specification, and in both cases a verdict that survives the mutation proves the mutated part was not load-bearing. Beer/Ben-David/Eisner/Rodeh (FMSD 18:141–163, 2001) give the logic-independent definition; Chockler/Kupferman/Vardi (FMSD 28:189–212, 2006) the coverage half.
That is our recurring fault class — a stated guarantee is not enforced on the path that executes — stated 25 years before we hit it.
The honest split (do not present adopting this as research — it is catching up):
- Solved practice: "which parts of the model/assumptions did this proof actually depend on" — commodity in hardware FV (Cadence JasperGold ProofCore, Synopsys VC Formal formal-core coverage, Siemens Questa PropCheck), formalized for software as Inductive Validity Cores (Ghassabani/Gacek/Whalen, FSE'16, arXiv:1603.04276), shipping in Kind 2/JKind at ~17–52% proof-time overhead, and in Dafny as
--warn-contradictory-assumptions / --warn-redundant-assumptions.
- Open: "is this specification strong enough / does this model faithfully describe the machine" — no mechanical adequacy metric exists; the state of the art is differential validation plus coverage of the semantics model itself (Sail/ARM-ASL, POPL'19).
Yield, cited carefully: IBM Haifa reported that in early formal runs on a new design "typically 20% of formulas are found to be trivially valid, and trivial validity always points to a real problem." That is reported industrial experience over several years, not a measured study — cite it as such, never as "measured".
Governance advice (Google SoC formal sign-off, DVCon Taiwan 2023): run adequacy checks coarse→fine — over-constraint → COI → proof-core → fault-injection/mutation → bounded-depth — and reserve the expensive mutation step for milestones, not every commit.
🤖 Filed via Claude Code from a deep-research pass on vacuity/adequacy checking.
Ask
Make axiom auditing a first-class, default-on gate in the Lean rules, so a proof target cannot silently depend on
sorryAxor an unexpected axiom. Today this is a discipline that each repo re-implements by hand (ordeal checks it manually inlean/Sound.lean; gale's honesty ledger records that Lean proofs are "local only, no CI record"). As a Bazel rule it becomes automatic for every consumer.Why this is the highest-value check for Lean specifically
Lean's kernel already computes the answer —
#print axioms fooreturns exactly the axioms a theorem transitively depends on. The vacuity failure it catches is total: a theorem that depends onsorryAxis not proved at all, yetlake buildis green and the file looks finished. This is the cheapest possible instance of "the proof did not depend on what you think it did".Proposed rule features
lean_proof_test/ an attribute on the existing test rule — axiom allowlist.Per-target
allowed_axioms = ["propext", "Classical.choice", "Quot.sound"](the standard classical trio), defaulting to exactly that set. The rule runs#print axiomsover the declared theorems and fails the build if any other axiom appears —sorryAxabove all. Emit the offending declaration and its axiom set in the failure message.sorrysyntactically as well as semantically. Asorryin a definition used by a proof, or in an unexported lemma, may not surface in the top-level theorem's axiom set. Cheap complementary grep-level check, opt-out per target.<target>.axioms.json) so downstream tooling (rivet evidence, an honesty ledger, a claim-check predicate) can consume "what does this proof actually rest on" as evidence, not prose. This is the piece that makes the gate composable across the org.--warn-redundant-assumptions: a hypothesis in scope that no proof goal required is a signal the theorem is weaker than its statement suggests. Report, don't fail.Notes
sorry-free and axiom-clean against{propext, Classical.choice, Quot.sound}— this rule would make that the default posture rather than a per-repo achievement.allowed_axioms = [...]) keeps it honest by forcing the exception to be written down in the BUILD file, where review sees it.Background: the research this comes from
A survey of vacuity/adequacy checking (state of the art, primary sources) produced one framing worth internalising, from Kupferman's Sanity Checks in Formal Verification (CONCUR'06): coverage and vacuity are the same check applied to opposite operands — coverage mutates the system, vacuity mutates the specification, and in both cases a verdict that survives the mutation proves the mutated part was not load-bearing. Beer/Ben-David/Eisner/Rodeh (FMSD 18:141–163, 2001) give the logic-independent definition; Chockler/Kupferman/Vardi (FMSD 28:189–212, 2006) the coverage half.
That is our recurring fault class — a stated guarantee is not enforced on the path that executes — stated 25 years before we hit it.
The honest split (do not present adopting this as research — it is catching up):
--warn-contradictory-assumptions/--warn-redundant-assumptions.Yield, cited carefully: IBM Haifa reported that in early formal runs on a new design "typically 20% of formulas are found to be trivially valid, and trivial validity always points to a real problem." That is reported industrial experience over several years, not a measured study — cite it as such, never as "measured".
Governance advice (Google SoC formal sign-off, DVCon Taiwan 2023): run adequacy checks coarse→fine — over-constraint → COI → proof-core → fault-injection/mutation → bounded-depth — and reserve the expensive mutation step for milestones, not every commit.
🤖 Filed via Claude Code from a deep-research pass on vacuity/adequacy checking.