Ask
Verus is SMT-backed, which makes it the repo where the #1 adoptable technique from the vacuity survey applies most directly: proof-dependency / unsat-core analysis. Two gates, both reusing the same machinery:
- Contradictory-assumption detection — the classic vacuous proof. If the assumptions in scope at a program point are contradictory (or the point is unreachable), everything verifies there and the proof means nothing.
- Redundant-assumption / unsat-core coverage — report which
requires clauses, assumes, and model parts the proof actually needed; treat the complement as unverified.
The prior art to copy
Dafny already ships exactly this, and names the failure mode better than we could (Dafny proof-dependency blog):
"If it's possible to construct a proof that the property holds without considering what we're ultimately trying to prove, we say that we've proved it vacuously. This can occur because the assumptions in scope at that program location are contradictory, or that that location is unreachable."
--warn-contradictory-assumptions — warns whenever a proof completes without taking the goal into account.--warn-redundant-assumptions — warns when an assumption in scope (from assume or requires) was not required to complete any proof goal.
Both are Dafny/Boogie/Z3 — the same stack Verus sits on, so the mechanism transfers rather than needing invention. The theory generalization is Inductive Validity Cores (Ghassabani/Gacek/Whalen, FSE'16, arXiv:1603.04276), which explicitly propose proof cores as a semantic vacuity detector: "even if a property is not syntactically vacuous, it may not require substantial portions of the model. This in turn may indicate that either a) the model is incorrectly constructed or b) the property is weaker than expected." Measured overhead when piggybacking on the solver's existing UNSAT-core facility: ~17% (Z3) / ~52% (Yices) — cheap enough for CI. Certora ships the same idea commercially as Rule Sanity Checks (vacuity check + assertion-tautology check).
Proposed rule features
verus_verify attribute check_vacuity = True (default on). Surface Verus/Z3's unsat-core so the rule can fail, or at minimum warn loudly, when a proof completes without depending on its goal.- Trusted-base counting as a gate. Count
#[verifier::external_body], assume(...), and assume_specification per target and fail if the count exceeds a recorded maximum (max_external_body = N). This is the count-max predicate pattern we already use for claim-checking, moved into the build. It stops the trusted base growing silently — which is precisely how a "verified" component quietly stops being one.
- Machine-readable proof-dependency output (
<target>.proofdeps.json): which requires/assumes were load-bearing, which were not. Consumable as rivet evidence and by an honesty ledger.
- A sanity assert helper (cheap, do first). The poor-man's version, available today with zero tooling: in a proof context where vacuity is suspected,
assert(false) must fail. If it succeeds, the context is contradictory and every proof there is vacuous. Worth a documented macro/idiom in the rules even before (1) lands.
Ordering
Item 4 costs nothing and can ship immediately. Items 1–3 are the real work; follow the industrial ordering (Google SoC formal sign-off, DVCon 2023) — cheap structural checks every commit, expensive mutation/fault-injection only at milestones.
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
Verus is SMT-backed, which makes it the repo where the #1 adoptable technique from the vacuity survey applies most directly: proof-dependency / unsat-core analysis. Two gates, both reusing the same machinery:
requiresclauses,assumes, and model parts the proof actually needed; treat the complement as unverified.The prior art to copy
Dafny already ships exactly this, and names the failure mode better than we could (Dafny proof-dependency blog):
--warn-contradictory-assumptions— warns whenever a proof completes without taking the goal into account.--warn-redundant-assumptions— warns when an assumption in scope (fromassumeorrequires) was not required to complete any proof goal.Both are Dafny/Boogie/Z3 — the same stack Verus sits on, so the mechanism transfers rather than needing invention. The theory generalization is Inductive Validity Cores (Ghassabani/Gacek/Whalen, FSE'16, arXiv:1603.04276), which explicitly propose proof cores as a semantic vacuity detector: "even if a property is not syntactically vacuous, it may not require substantial portions of the model. This in turn may indicate that either a) the model is incorrectly constructed or b) the property is weaker than expected." Measured overhead when piggybacking on the solver's existing UNSAT-core facility: ~17% (Z3) / ~52% (Yices) — cheap enough for CI. Certora ships the same idea commercially as Rule Sanity Checks (vacuity check + assertion-tautology check).
Proposed rule features
verus_verifyattributecheck_vacuity = True(default on). Surface Verus/Z3's unsat-core so the rule can fail, or at minimum warn loudly, when a proof completes without depending on its goal.#[verifier::external_body],assume(...), andassume_specificationper target and fail if the count exceeds a recorded maximum (max_external_body = N). This is thecount-maxpredicate pattern we already use for claim-checking, moved into the build. It stops the trusted base growing silently — which is precisely how a "verified" component quietly stops being one.<target>.proofdeps.json): whichrequires/assumes were load-bearing, which were not. Consumable as rivet evidence and by an honesty ledger.assert(false)must fail. If it succeeds, the context is contradictory and every proof there is vacuous. Worth a documented macro/idiom in the rules even before (1) lands.Ordering
Item 4 costs nothing and can ship immediately. Items 1–3 are the real work; follow the industrial ordering (Google SoC formal sign-off, DVCon 2023) — cheap structural checks every commit, expensive mutation/fault-injection only at milestones.
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.