Mutation testing over Aeneas-verified Rust — is proof-adequacy checking via mutation viable?

[avrabe]

Independent research spike, not tied to a specific bug. Written as a genuine second opinion on a colleague's proposal — investigated from scratch, cited where I actually found something, flagged plainly where I didn't.

Context

A colleague proposed layering mutation testing on top of the Aeneas pipeline this repo is building (rules_lean#1): take Rust source, generate small syntactic mutants (flip a comparison operator, change a constant, swap +/-, delete a statement — the standard mutation-testing operator set), push each mutant through charon_llbc → aeneas_translate → the existing hand-written Lean proofs/specs for that function, and treat "proof still holds against the mutant" as a signal that the spec is too weak to have caught the change — a mutation-based adequacy/vacuity check for the proofs themselves, on top of (not instead of) whatever mutation testing the Rust test suite already gets from something like cargo-mutants.

This issue answers five questions with real citations, then gives a verdict and a scoped first step.

1. Is this a named technique in the formal methods literature?

Yes, under several names, none of which are specific to Rust:

• Vacuity checking / vacuity detection — the canonical formal-methods framing of "the property holds, but for a trivial/uninteresting reason." Seminal work: Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh, "Efficient Detection of Vacuity in ACTL Formulas," CAV 1997 (LNCS 1254, pp. 279–290), journal version "Efficient Detection of Vacuity in Temporal Model Checking," Formal Methods in System Design 18(2), 2001, pp. 141–163. This is about antecedent failure in temporal logic, not mutation — but it's the direct conceptual ancestor of "the proof passed, but did it actually exercise the thing we care about?"
• Mutation testing of formal specifications is an established sub-area:
  • Alloy: Allison Sullivan, Kaiyuan Wang, Razieh Nokhbeh Zaeem, Sarfraz Khurshid, "Automated Test Generation and Mutation Testing for Alloy," ICST 2017; Kaiyuan Wang, Allison Sullivan, Sarfraz Khurshid, "MuAlloy: A Mutation Testing Framework for Alloy," ICSE 2018 (demo); Aleksandar Jovanovic, Allison Sullivan, "Mutation Testing for Temporal Alloy Models," MODELS 2023, extended version in Software and Systems Modeling 24, pp. 1847–1868 (2024).
  • Model-based/Event-B-adjacent: symbolic model-based mutation testing combining reachability and refinement checking (arXiv:1202.6123).
  • Classic NIST lineage on specification mutation for test generation: Paul Ammann, Paul E. Black, William Majurski, "Using Model Checking to Generate Tests from Specifications," ICFEM 1998, pp. 46–54; Vadim Okun, "Specification Mutation for Test Generation and Analysis," PhD thesis, U. Maryland Baltimore County, 2004.
  • Tzu-Chien Lee, Pao-Ann Hsiung, "Mutation Coverage Estimation for Model Checking," ATVA 2004 (LNCS 3299) — mutate the state graph, check whether the property set is still sensitive to it. This is model-checking-flavored, but structurally identical to the hypothesis in the proposal.
• Closest direct restatement of the hypothesis: Maxime Cordy, Sami Lazreg, Axel Legay, Pierre-Yves Schobbens, "Towards Strengthening Formal Specifications with Mutation Model Checking," ESEC/FSE 2023 (NIER track), doi:10.1145/3611643.3613080. Quote (from their abstract): specifications are judged "not strong enough if they fail to detect faults in purposely mutated models" — and their two case studies show a spec catching only 40% and 60% of randomly generated mutants respectively. This is essentially the exact experiment the colleague is proposing, run on model-checking specs, published two years ago at a top SE venue, with a concrete empirical result showing the signal is real (specs really can be that leaky).
• Directly on a proof assistant (the closest structural analog to what we'd be doing to Lean): Ahmet Celik, Karl Palmskog, Marinela Parovic, Emilio Jesús Gallego Arias, Milos Gligoric, "Mutation Analysis for Coq," ASE 2019. They coin the term "mutation proving" and ship a tool, MCoq, that mutates Coq developments and checks whether the existing proof scripts still go through. Coq is Lean's closest theorem-proving relative, so this is the strongest available precedent for "mutate the artifact under a proof assistant, re-check the existing proofs" — just not for Rust/Aeneas/Lean specifically.
• Also found: Arun Chakrapani Rao, A. Raouf, Gunwant Dhadyalla, Vijay S. Pasupuleti, "Mutation testing based evaluation of formal verification tools," DSA 2017 (doi:10.1109/DSA.2017.10); Serge Demeyer, Ali Parsai, Sten Vercammen, Brent van Bladel, Mehrdad Abdi, "Formal Verification of Developer Tests: A Research Agenda Inspired by Mutation Testing," ISoLA 2020.

Verdict on Q1: yes, real, named, and multiply-invented across sub-communities (model checking, Alloy, Coq). It is not a single canonical technique with one name — it's independently reinvented every time a formal-methods community notices the same problem test engineers noticed in 1978 (see Q4).

2. Has this been discussed for Rust verifiers (Kani, Verus, Creusot, Prusti) specifically?

Partially, and not in the mutation-testing form:

• Kani ships a real, named vacuity-adjacent feature: kani::cover, documented in "Checking Code Reachability and Sanity Checking Proof Harnesses with kani::cover," Kani Rust Verifier Blog, Jan 30 2023. It explicitly uses the word "vacuous": a harness author may have doubts about "whether the proof harness they wrote is vacuous, e.g. does it cover the entire input space." The mechanism is reachability/SAT-based (assert!(!condition) internally), not mutation-based, and the post does not cite the model-checking vacuity literature in Q1 — it looks like an independent reinvention, not a citation of it.
• Dafny (same Microsoft Research "verification-aware languages" lineage as Verus/F*) has a directly relevant blog post: "Identifying specification problems in Dafny programs," Dafny Blog, Oct 27 2023 — a static "proof dependencies" tool for the same underlying concern (over-constrained preconditions, unreachable code, redundant assumptions making a proof pass vacuously), again not mutation-based.
• Closest published match to the actual proposed technique, and the best citation for "this idea is alive in the Rust-verification-adjacent research community": Shuvendu K. Lahiri (Microsoft Research), "Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages," FMCAD 2024. It proposes, as a completeness metric for Dafny/F*-style specs, "mutating values in test cases to check if the specification still holds." This is verification-aware-language work, not Rust/Verus/Kani specifically, but it's the nearest thing found to the exact mechanism proposed here, from a credible verification researcher, at a real FM venue, 2024.
• Not substantiated: no GitHub issue, discussion, RFC, or blog post was found that ties cargo-mutants to Kani, Verus, Creusot, or Prusti, and no evidence that any of those four communities runs or discusses mutation testing over proof harnesses as a documented practice. Searched Kani's and Verus's repos/blogs directly; came up empty. If it's being discussed informally (Zulip, Discord), it isn't showing up in indexed search.
• One indirect but real data point: Kani compiles proof harnesses down to CBMC's GOTO-program model checker (confirmed via Kani's own architecture docs / arXiv:2607.01504). Alex Groce, Iftekhar Ahmed, Carlos Jensen, et al., "How Verified (or Tested) is My Code? Falsification-Driven Verification and Testing," ASE 2015 / extended in Automated Software Engineering 25, 2018, pp. 917–960 — ran mutation-style falsification analysis directly against CBMC, the same backend engine Kani itself uses. So the engine underneath Kani has precedent for this kind of analysis; Kani-the-Rust-tool does not.

3. Anything combining Aeneas/Charon with mutation testing or vacuity checking?

No. Searched AeneasVerif/aeneas and AeneasVerif/charon issue trackers directly (gh search issues --repo AeneasVerif/... mutation, ... vacuous) — no hits related to either term. Searched the academic literature for "Aeneas" + "mutation testing" and "Charon"/"LLBC" + "mutation" — nothing. The founding paper, Son Ho and Jonathan Protzenko, "Aeneas: Rust Verification by Functional Translation," ICFP 2022 / PACMPL 6(ICFP), pp. 711–741 (arXiv:2206.07185), doesn't mention mutation testing or vacuity checking. This is a genuinely open niche — not a rediscovery of prior art, but also not something anyone has validated on this exact toolchain.

4. Known pitfalls

Two real ones, both with citations, and one of them is a documented risk specific to this repo's current state:

• Equivalent mutants. Classic, unsolved-in-general problem: R. A. DeMillo, R. J. Lipton, F. G. Sayward, "Hints on Test Data Selection: Help for the Practicing Programmer," IEEE Computer 11(4), 1978, pp. 34–41 (introduces the coupling effect and the equivalent-mutant problem); A. J. Offutt, J. Pan, "Automatically Detecting Equivalent Mutants and Infeasible Paths," Software Testing, Verification and Reliability 7(3), 1997, pp. 165–192 (partial/heuristic detection only — the general problem reduces to path feasibility, which is undecidable in general). Y. Jia, M. Harman, "An Analysis and Survey of the Development of Mutation Testing," IEEE TSE 37(5), 2011, pp. 649–678, is the standard survey confirming this is still an open cost driver three decades later. It's worse here than in ordinary mutation testing because the "kill check" isn't a millisecond test run — it's a full charon_llbc → aeneas_translate → Lean type-check/proof-replay, likely seconds-to-minutes per mutant. Classic cost-reduction techniques (selective mutation, weak mutation, schema-based mutation — A. J. Offutt, R. H. Untch, "Mutation 2000: Uniting the Orthogonal," in Mutation Testing for the New Century, Springer, 2001, pp. 34–44) were designed assuming cheap re-execution against a compiled test suite; none of them were designed against a "re-execution" step that's a theorem-proving pipeline, so the cost math needs to be redone, not reused, before this scales past a handful of mutants.
• Toolchain-immaturity confusion — the one that actually matters for us. rules_lean#1 already documents (citing AeneasVerif/charon#142) that Charon currently rejects or mistranslates: unsafe code, GATs, RPITIT, Drop semantics, thread-locals, contract annotations, return/break/continue across nested loops, interior mutability, concurrency. A syntactic mutant that happens to touch or land near one of those edges will fail to translate for reasons that have nothing to do with whether the mutant is semantically distinguishable by the spec. A naive harness that buckets outcomes into just "proof survived" vs. "proof killed" will silently misclassify "Charon choked" as either a false kill or, worse, get discarded and quietly deflate the mutant sample — either way, the measured vacuity rate stops being a statement about spec quality and becomes partly a statement about Charon's Nov-2024-vintage maturity. Any prototype must bucket outcomes into at minimum: (a) translation failure (toolchain limitation — discard, don't count), (b) generated Lean fails to build/typecheck against the mutant (usually a proof that references specific generated structure — discard/inspect, don't count as a kill or a survival), (c) proof re-succeeds against the mutant (real signal — spec gap), (d) proof fails against the mutant (real signal — mutant killed, spec adequate for this case). Collapsing (a)/(b) into (c) is exactly the trap the task asked me to check for, and it's real and current for this repo specifically, not hypothetical.

5. Real industrial precedent (hardware EDA)

Yes, and it's the strongest, most literal precedent found for the whole idea — just aimed at RTL, not Rust:

• Cadence markets this by name today: the Jasper Design Coverage Verification App product page (cadence.com) advertises "cone-of-influence, mutation, and unique Proof Core technology" as its three named coverage techniques for measuring how completely an assertion set verifies a design. A Cadence patent, US 8,990,746 B1, "Method for mutation coverage during formal verification" (inventors Pradeep Goyal, Alok Jain; filed Mar 26 2014, granted Mar 24 2015), describes the actual algorithm: inject mutants into an assertion's cone of influence, run the formal engine, and use constraint solving to iteratively determine which mutants the assertion set actually catches — i.e., mutate the design, re-verify, and treat "still holds" as a coverage gap. This is the exact structure of the proposal, industrially deployed and patented over a decade ago.
• Synopsys VC Formal documents an equivalent "mutation coverage" capability: applying mutations to the design and checking whether assertions fail, explicitly used to flag over-constrained scenarios (a close cousin of the "vacuity" concern in Q1/Q2). See Synopsys's "Unlocking Formal Signoff Methodology" whitepaper and related VC Formal materials.
• Siemens Questa: has a broader "Formal Verification Suite" / coverage app (Questa Increase Coverage), but I could not confirm a specifically-branded "mutation coverage" feature name for Questa the way I could for Cadence and Synopsys — flagging this explicitly rather than asserting it.
• A 2024 academic example shows the same loop being actively used with LLM-generated properties: Muhammad Hassan, Sallar Ahmadi-Pour, Khushboo Qayyum, Chandan Kumar Jha, Rolf Drechsler, "LLM-Guided Formal Verification Coupled with Mutation Testing," DATE 2024 — mutate the RTL design under verification, check whether an LLM-generated invariant still holds, use survival as a quality signal on the invariant.

This is real, confirmed, and current — not a hypothetical analogy. The EDA industry has been doing "mutate the artifact, re-verify, treat still-holds as a coverage gap" as a shipped, marketed, patented product feature for over a decade.

Verdict

Credible and research-grounded as a concept — it has real names (vacuity checking, mutation model checking, mutation proving), a real direct restatement in the SE literature from 2023 with empirical numbers backing the hypothesis (Cordy et al.), a direct proof-assistant precedent (Celik et al.'s MCoq for Coq), and a decade-plus of literal industrial deployment in hardware formal verification (Cadence/Synopsys). It is not something anyone has built or even discussed for the Aeneas/Charon/Lean stack specifically — that part is a genuinely open niche, confirmed by direct search of the AeneasVerif GitHub org and the academic literature, not a rediscovery. The two pitfalls are real and, for the immaturity-confusion one specifically, not hypothetical for this repo — Charon's own documented translation gaps (already tracked in rules_lean#1) make "toolchain choked" vs. "mutant survived" a live methodological trap here today, not a someday concern.

Net: worth a small, bounded prototype. Not worth building mutant-generation automation or CI wiring yet — the cost-per-mutant (full theorem-proving re-run) and the confusability trap above mean we should measure real base rates by hand on a handful of mutants before investing in tooling.

Recommendation — scoped first step

Blocked by rules_lean#1 (needs a working end-to-end charon_llbc → aeneas_translate → Lean pipeline with at least one hand-written proof on the other end — Stage 4/5 there, sigil Ed25519 or gale ring_buf).

Once that lands:

• Hand-pick one already-translated function with an existing hand-written Lean proof (sigil Ed25519 or gale ring_buf, per rules_lean#1 Stage 4/5).
• Hand-write (not auto-generate) ~10–20 classic mutants of the Rust source: relational/arithmetic operator swap, off-by-one boundary constant, statement deletion, +/- swap. Pre-classify each by hand as {expected-kill, expected-equivalent, unsure} before running anything.
• Run each mutant through the existing pipeline and bucket every outcome into the four buckets from Q4: translation failure / Lean build failure / proof re-succeeds / proof fails. Record which bucket by hand.
• Report the empirical split (how many landed in each bucket, and whether "unsure" mutants clustered around Charon's known gaps from AeneasVerif/charon#142).
• Only if the "proof re-succeeds" bucket turns up genuine, non-equivalent spec gaps on this small sample does it make sense to invest further (mutant-generation tooling, CI wiring, an equivalent-mutant filter) — otherwise document the finding and close it out, the same way rules_lean#3 scoped its "first useful pass" against the MIRAI prototype before committing months of effort.

Non-goals (for now)

• Building automated mutant-generation tooling (a Rust-level equivalent of cargo-mutants wired into Bazel) before the manual prototype above produces a real signal.
• Treating this as a replacement for the test suite's own mutation testing (cargo-mutants or equivalent) — it's explicitly a layer on top, checking the proofs, not the tests.
• Claiming parity with the EDA tools' mutation-coverage features — those operate on a bounded RTL cone of influence with mature constraint-solving infrastructure refined over a decade; our per-mutant cost (Charon + Aeneas + Lean) is not that.

References

• Beer, Ben-David, Eisner, Rodeh, "Efficient Detection of Vacuity in ACTL Formulas," CAV 1997; journal version, Formal Methods in System Design 18(2), 2001.
• Sullivan, Wang, Zaeem, Khurshid, "Automated Test Generation and Mutation Testing for Alloy," ICST 2017.
• Wang, Sullivan, Khurshid, "MuAlloy: A Mutation Testing Framework for Alloy," ICSE 2018.
• Jovanovic, Sullivan, "Mutation Testing for Temporal Alloy Models," MODELS 2023; extended version, Software and Systems Modeling 24, 2024.
• Ammann, Black, Majurski, "Using Model Checking to Generate Tests from Specifications," ICFEM 1998.
• Okun, "Specification Mutation for Test Generation and Analysis," PhD thesis, UMBC, 2004.
• Lee, Hsiung, "Mutation Coverage Estimation for Model Checking," ATVA 2004.
• Cordy, Lazreg, Legay, Schobbens, "Towards Strengthening Formal Specifications with Mutation Model Checking," ESEC/FSE 2023 NIER, doi:10.1145/3611643.3613080.
• Celik, Palmskog, Parovic, Gallego Arias, Gligoric, "Mutation Analysis for Coq," ASE 2019.
• Chakrapani Rao, Raouf, Dhadyalla, Pasupuleti, "Mutation testing based evaluation of formal verification tools," DSA 2017, doi:10.1109/DSA.2017.10.
• Demeyer, Parsai, Vercammen, van Bladel, Abdi, "Formal Verification of Developer Tests: A Research Agenda Inspired by Mutation Testing," ISoLA 2020.
• Lahiri, "Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages," FMCAD 2024.
• Kani Rust Verifier Blog, "Checking Code Reachability and Sanity Checking Proof Harnesses with kani::cover," Jan 30 2023.
• Dafny Blog, "Identifying specification problems in Dafny programs," Oct 27 2023.
• DeMillo, Lipton, Sayward, "Hints on Test Data Selection: Help for the Practicing Programmer," IEEE Computer 11(4), 1978.
• Jia, Harman, "An Analysis and Survey of the Development of Mutation Testing," IEEE TSE 37(5), 2011.
• Offutt, Untch, "Mutation 2000: Uniting the Orthogonal," in Mutation Testing for the New Century, Springer, 2001.
• Offutt, Pan, "Automatically Detecting Equivalent Mutants and Infeasible Paths," Software Testing, Verification and Reliability 7(3), 1997.
• Cadence, Jasper Design Coverage Verification App product page (cadence.com).
• US Patent 8,990,746 B1, "Method for mutation coverage during formal verification," Cadence Design Systems Inc., 2015.
• Synopsys, "Unlocking Formal Signoff Methodology" whitepaper, VC Formal.
• Hassan, Ahmadi-Pour, Qayyum, Jha, Drechsler, "LLM-Guided Formal Verification Coupled with Mutation Testing," DATE 2024.
• Ho, Protzenko, "Aeneas: Rust Verification by Functional Translation," ICFP 2022 / PACMPL 6(ICFP) (arXiv:2206.07185).
• AeneasVerif/charon#142 (known translation gaps, already cited in rules_lean#1).
• AeneasVerif/aeneas, AeneasVerif/charon issue trackers, searched directly for "mutation" / "vacuous" (no hits, as of this research).

Related

• rules_lean#1 — Aeneas end-to-end pipeline (blocker; this needs a working pipeline first)
• rules_lean#3 — Charon-based abstract interpretation (sibling exploratory/strategic issue, same "scope a first useful pass before committing months" shape)

[avrabe]

Independent triangulation update: I ran a second, fully independent deep-research pass (107-agent adversarial verification workflow) blind to this issue's findings, then personally fetched and read the two most decision-relevant primary sources directly. Net result: this issue's verdict holds, and two of its citations are now confirmed with more precision than before; two others turned out not to hold up and should be corrected.

Confirmed, with exact primary-source detail (I read the full PDF/patent myself):

• Cordy, Lazreg, Legay, Schobbens, "Towards Strengthening Formal Specifications with Mutation Model Checking," ESEC/FSE '23 (doi:10.1145/3611643.3613080) — real paper, exact title/authors/DOI. Their own abstract: "their specification can only detect 40% and 60% of randomly generated mutants." Table 1 gives the precise figures: Minepump mutation score = 61.458% (88 mutants), ADAPRO = 39.803% (406 mutants) — ADAPRO is real CERN/ALICE detector-control software, not a toy exemplar. This is the closest direct structural match to the proposal in this issue (mutate the model, re-check the existing spec, "survives" = spec gap), just on LTL/model-checking specs rather than Lean proofs.
• US Patent 8,990,746 B1, "Method for mutation coverage during formal verification" (Cadence, inventors Pradeep Goyal & Alok Jain, filed 2014-03-26, granted 2015-03-24) — every detail confirmed exactly against Google Patents. Mechanism, read directly: inject faults into an assertion's cone of influence, then use constraint-guided formal verification (not brute-force one-mutant-at-a-time) to determine which mutations the assertion set actually catches. Same core idea as this issue proposes, patented and shipped in hardware EDA for over a decade. (I could not independently confirm Cadence's product-page marketing wording — that specific fetch was blocked by the site — so treat "Jasper markets this as 'mutation coverage'" as plausible-but-unconfirmed-by-me, not verified.)

Also independently reconfirmed (via the adversarial workflow, 3-0 votes): the Beer/Ben-David/Eisner/Rodeh CAV 1997 vacuity paper exists exactly as cited, and — most importantly — Celik, Palmskog, Parovic, Gallego Arias, Gligoric, "Mutation Analysis for Coq" (ASE 2019) is confirmed verbatim, including the term "mutation proving," the tool name MCoq, and a direct quote that states almost exactly this issue's hypothesis: a surviving mutant can show "an ostensibly strong and complete lemma about a function can be proven regardless of what the returned value is." The paper explicitly roots this in the vacuity-checking lineage (citing Ball & Kupferman, "Vacuity in testing," 2008) — Coq being Lean's closest theorem-prover relative, this remains the single strongest analog to what's proposed here for Aeneas/Lean.

Correction — two things do NOT hold up on adversarial re-verification, don't repeat them:

• The framing of Beer et al. 1997 as "the first/foundational" vacuity paper, and a specific "~20% of formulas at IBM came back vacuously valid" statistic, were both explicitly refuted (voted down 1-2) when checked against the primary source. Cite the paper for its content, not for either of those two framings.
• A claim that Charon's documented gaps (unsafe code, GATs, RPITIT — issue Tracking issue for unsupported rust features AeneasVerif/charon#142) are "now resolved" was also refuted. This matters directly for this issue's pitfall Add Charon toolchain (Stage 1) + Lean 4.29.1 bump #2: the risk of a mutant failing to translate through Charon being misclassified as a mutant that survived the proof is not a someday concern — it's live and unresolved today. We have first-hand confirmation of exactly this failure class in this repo already: the relay-coverage CI job (real relay CRC32 code) hit an Aeneas internal error specifically on a const-eval'd global array — a case where the toolchain choked, not where a proof was weak. Any prototype here must bucket outcomes as this issue already specifies (translation failure / Lean build failure / proof re-succeeds / proof fails) and discard the first two — this isn't a hypothetical edge case, it's something this exact pipeline has already done.

No change to the recommendation: small, hand-curated manual prototype (~10-20 mutants) once the pipeline is stable, bucketed by hand, before any automation investment.