Replication package: Auditing LLM-Generated Proof Harnesses for Bounded Model Checking using Differential Mutation Analysis

Replication package for the paper *Auditing LLM-Generated Proof Harnesses forBounded Model Checking using Differential Mutation Analysis*. The package holds the differential mutation oracle, the expert and generated proofharnesses, every mutant with its per-mutant CBMC verdict, the prompts, the unwindbounds, the pinned tool versions and both corpora as the oracle read them. Onescript recomputes every number, table cell and plotted value in the paper from theraw verdicts. Start with `REPRODUCE.md`. It gives three levels, each slower than the last: 1. Check the paper against the released verdicts in minutes, with no model checker: `bash scripts/audit_all.sh`.2. Re-decide every CBMC verdict in about six hours under CBMC 6.4.0.3. Regenerate the harnesses, which needs model API calls. Contents: - `evaluation/` — the per-mutant verdicts every number comes from.- `scripts/paper_numbers_640.py` — the audit registry: every number in the paper next to the computation that produces it.- `corpus/aws-c-common` and `corpus/s2n-tls` — the corpora as the oracle read them, with a sha256 manifest.- `paper/paper.tex` — the submitted source, which three of the audits read. Licensing: the scripts, the generated harnesses and the derived data are releasedunder Apache-2.0. `corpus/aws-c-common` and `corpus/s2n-tls` are Amazon's, alsoApache-2.0, redistributed with their LICENSE and NOTICE files; the mutants arederived from them. This version is anonymous, for double-anonymous review. ## Copyright box Copyright (C) 2026 The Authors.