Artifact
evidence-audit
A grader for recorded verification outputs that reports what a run explored, not the verdict it printed.
What it establishes
That recorded outputs from Kani, loom and cargo test, and recorded Lean artifacts, can be graded on what the run actually explored, and that three real green runs could not have failed.
What it does not establish
No defect in the subject crates is claimed. The tool runs no verifier and reads recorded outputs only. Version 0.1.
Method
Three committed case studies with inputs, patches, outputs and reproduction commands; grading by reachability, interleaving counts and value lemmas.
Results
Kani assertion UNREACHABLE after the first injected bug; loom 9 uninstrumented against 54 instrumented interleavings with byte-identical verdicts; Lean axiom audits byte-identical for a correct and a wrong model.
What has to be trusted
The recorded outputs themselves and the tool's parsers; the case-study patches.
Prior work
Vacuity detection and coverage metrics for model checking. The contribution is grading recorded outputs across four tools with the catches committed as fixtures.
Reproduce it
pip install -e . && python3 -m pytest tests/ -q
Findings drawn from this artifact are on the evidence ledger.