Add a flag for vacuity check

[pennyannn]

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

Add vacuity checking (-V check-vacuity)

Summary

This PR adds a new flag -V check-vacuity that detects vacuous proofs — proofs that succeed only because the assumptions are contradictory, not because the conclusion actually follows.

Motivation

When a function's requires clauses, trait bounds, type invariants, or call postconditions are contradictory, any ensures clause is trivially provable. This can hide real specification bugs, especially when using external_body or assume_specification with incorrect ensures clauses.

Approach

The implementation follows the Dafny/Boogie approach for detecting contradictory assumptions, adapted for Verus's architecture.

When the flag is enabled, after a successful normal verification, Verus runs a second SMT query using a Boogie-style tracked WP encoding:

• Each assume H becomes (v ==> H) ==> rest with a tracked boolean v
• Each assert G becomes (a ∧ G) ∧ rest with a tracked boolean a
• Each local axiom (requires, trait bounds, type invariants) becomes (v ==> axiom) with a tracked boolean v

Each tracking variable is asserted as (assert (! v :named vacuity$v)) so it appears in the SMT unsat core. After check-sat returns unsat, the unsat core reveals which tracking variables were needed. If any assertion's tracking variable is absent, that assertion was proved without needing the goal — the assumptions are contradictory.

The IMPLIES encoding for assumptions and AND encoding for assertions is essential due to how negation interacts with the WP structure. See source/VACUITY.md for a detailed explanation with examples.

Output

Given this input with one correct and one vacuous function:

proof fn good(x: int)
    requires x > 3,
    ensures x >= 3,
{}

proof fn bad(x: int)
    requires x > 10, x < 5,
    ensures x == 42,
{}

The output is:

error: function body check: vacuity check failed: the hypotheses are inconsistent (they imply false), so the proof is vacuously true
  --> test.rs:7:7
   |
 7 | proof fn bad(x: int)
   |       ^^^^^^^^^^^^^^

verification results:: 2 verified, 0 errors
vacuity check:: 1 passed, 1 errors

• good: verified successfully, vacuity check passed
• bad: verified successfully (contradictory requires make any ensures trivially true), but vacuity check caught it — counted as 1 error in both lines

When all functions are correct:

verification results:: 2 verified, 0 errors
vacuity check successful:: 2 passed, 0 errors

Testing

• 145 AIR unit tests pass (140 existing + 5 new)
• 21 Verus integration tests pass (all new)
• All existing tests unaffected (flag defaults to off)

Reference

Aaron Tomb and Anjali Joshi. "Static Coverage in Deductive Software Verification." In Formal Methods in Computer-Aided Design (FMCAD), 2025.

[briangmilnes]

Although I can check a lot with veracity minimize libs this is a big step forward. I would love to know if any of my vstd plus library has inconsistencies.

…

On Mon, Apr 6, 2026, 6:27 PM Yan Peng ***@***.***> wrote: By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license <https://github.com/verus-lang/verus/blob/main/LICENSE>. Add vacuity checking (-V check-vacuity) Summary This PR adds a new flag -V check-vacuity that detects vacuous proofs — proofs that succeed only because the assumptions are contradictory, not because the conclusion actually follows. Motivation When a function's requires clauses, trait bounds, type invariants, or call postconditions are contradictory, any ensures clause is trivially provable. This can hide real specification bugs, especially when using external_body or assume_specification with incorrect ensures clauses. Approach The implementation follows the Dafny/Boogie approach for detecting contradictory assumptions, adapted for Verus's architecture. When the flag is enabled, after a successful normal verification, Verus runs a second SMT query using a Boogie-style tracked WP encoding: - Each assume H becomes (v ==> H) ==> rest with a tracked boolean v - Each assert G becomes (a ∧ G) ∧ rest with a tracked boolean a - Each local axiom (requires, trait bounds, type invariants) becomes (v ==> axiom) with a tracked boolean v Each tracking variable is asserted as (assert (! v :named vacuity$v)) so it appears in the SMT unsat core. After check-sat returns unsat, the unsat core reveals which tracking variables were needed. If any assertion's tracking variable is absent, that assertion was proved without needing the goal — the assumptions are contradictory. The IMPLIES encoding for assumptions and AND encoding for assertions is essential due to how negation interacts with the WP structure. See source/VACUITY.md for a detailed explanation with examples. Output Given this input with one correct and one vacuous function: proof fn good(x: int) requires x > 3, ensures x >= 3,{} proof fn bad(x: int) requires x > 10, x < 5, ensures x == 42,{} The output is: error: function body check: vacuity check failed: the hypotheses are inconsistent (they imply false), so the proof is vacuously true --> test.rs:7:7 | 7 | proof fn bad(x: int) | ^^^^^^^^^^^^^^ verification results:: 1 verified, 1 errors vacuity check:: 2 checked, 1 errors - good: verified successfully, vacuity check passed - bad: verified successfully (contradictory requires make any ensures trivially true), but vacuity check caught it — counted as 1 error in both lines When all functions are correct: verification results:: 2 verified, 0 errors vacuity check successful:: 2 checked, 0 errors Testing - 145 AIR unit tests pass (140 existing + 5 new) - 20 Verus integration tests pass (all new) - All existing tests unaffected (flag defaults to off) ------------------------------ You can view, comment on, or merge this pull request online at: #2307 Commit Summary - a9915ab <a9915ab> Add a flag for vacuity check File Changes (10 files <https://github.com/verus-lang/verus/pull/2307/files>) - *A* source/VACUITY.md <https://github.com/verus-lang/verus/pull/2307/files#diff-09313109b295ee16480e3ce27510b6d457f211b6f43def23a66b49289e57d7c1> (200) - *M* source/air/src/block_to_assert.rs <https://github.com/verus-lang/verus/pull/2307/files#diff-6210e0759bebf84cd5ee20438fb2b319da08b98f76afc0ab4407d5c32038297f> (137) - *M* source/air/src/context.rs <https://github.com/verus-lang/verus/pull/2307/files#diff-4fee287070902a029f2dea0aef25c3406038671f25769c24f9942ebf79aa90b5> (25) - *M* source/air/src/main.rs <https://github.com/verus-lang/verus/pull/2307/files#diff-51b26df72846563644b1e040530500a824fd46569e985ea614eb4c5f700a9ef7> (6) - *M* source/air/src/smt_verify.rs <https://github.com/verus-lang/verus/pull/2307/files#diff-bb8b07b3d10333accee4c1b46ca07a3d37d4b6be1902b3e6dd0a9ff650999266> (213) - *M* source/air/src/tests.rs <https://github.com/verus-lang/verus/pull/2307/files#diff-8ef9b1e5c7c904b6d3882eaca5f32424ea9636c77ed9456d0248e464238f1e62> (183) - *M* source/rust_verify/src/config.rs <https://github.com/verus-lang/verus/pull/2307/files#diff-19545d963a4ef121c1c8251f5e7d3593c0641eac7b2bb92bfcefc020f3a814b0> (8) - *M* source/rust_verify/src/verifier.rs <https://github.com/verus-lang/verus/pull/2307/files#diff-50a27b1c820b608530ce2c50204747ed9f8f7a23720fd78a7a262f49f5d95dd8> (38) - *M* source/rust_verify_test/tests/common/mod.rs <https://github.com/verus-lang/verus/pull/2307/files#diff-9161f257dd3362ff68be5a8ce16ae5e135b07565a457dcc283a8867a5db18b0a> (3) - *A* source/rust_verify_test/tests/vacuity.rs <https://github.com/verus-lang/verus/pull/2307/files#diff-19f0fdd2066dcf4db7f8982c347609186628ee3aff47170cbf446e490f0f2800> (356) Patch Links: - https://github.com/verus-lang/verus/pull/2307.patch - https://github.com/verus-lang/verus/pull/2307.diff — Reply to this email directly, view it on GitHub <#2307>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACKMDK4MHMPUELYY4X47L534URKPPAVCNFSM6AAAAACXOZVRBCVHI2DSMVQWIX3LMV43ASLTON2WKOZUGIYTIOJQGE3DINQ> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[pennyannn]

Things that could be implemented to further improve the user experience:

1. Currently, report of error is on function level. It would be nice to explore tracking unsat core assumptions and which program assertion could be vacuously proved, maybe through desugering of label as is described in the paper. Or something similar but tailored to Verus. For now, one can insert assert(false) in various program branches to find the assertion and resort to running the SMT query again to reverse engineer the unsat core.
2. Add an annotation to allow certain assertion to be skipped for vacuity check.