Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Automated Testing and Repair for Verified Compilers Generated by a Coding Agent

(authored by agents unless marked 🧑) Tag: rinard2026automated, paper

scope and trust

The paper presents ACDC (Automated Certificate Detection and Correction) for Axon, a Lean compiler generated by a coding agent. Axon combines verified translation, credible compilation (optimizations emit certificates), an executable ASM semantics, and unverified parser/printer interfaces. The paper says: “We present an agent based automated testing and repair system for verified compilers that contain four kinds of code: verified code, checked code, unverified code, and specification.” (Abstract, p.1). Its headline correctness proofs are conditional on the operational semantics, checker, Lean kernel, and generated executable code being faithful.

technique 1: differential ASM-semantics/printer testing

Use this when a compiler has a formal machine model and a text backend. The paper’s procedure is:

  1. Generate batches of random ASM sequences of 6–32 instructions, each batch carrying a fresh seed (Section IV-A, p.5).
  2. Choose immediates either as the random value (probability 1/3) or from an extremal-value pool (probability 2/3); initialize model and target-machine executions identically (Section IV-A, p.5).
  3. Simulate the sequence with Axon’s executable ASM semantics, print it, assemble/link/execute the text, and compare final states (Section IV-A, p.5).
  4. Classify a run as Match, Different Outcome, Assemble Fail, or Panic. For a defect, record the class, sequence, differing registers or assembler message, and the seed (Section IV-A, pp.5–6).
  5. Give records to a coding agent. The prompt requires reproducing the seed, auditing semantics, every proof consumer, and the agent’s instruction understanding, then validating on the triggering batch and a new-seed batch (Section IV-A, p.6).

The paper reports: “The initial 30 minute detect phase processes 8,200 assembly programs, 82% (6,760) of which trigger a defect.” (Section V-B, p.7). Five repairs followed; three changed the printer, one semantics, and one both. The second detect phase processed 4,600 programs with no defect. Examples include materializing large immediates, emitting actual source/destination registers, reducing shift amounts modulo 64, and correcting floating comparison flags; the Fcmp repair changed semantics/printer by +21/−5 lines and proofs by +24/−24 (Table I, p.7).

Inference: In Verus, the same oracle can be an exec Rust model and emitted assembly run, with a host-side harness comparing outputs; the proof-facing model remains a spec fn/lemma layer. Verus cannot certify the external assembler or hardware execution, so this remains differential testing evidence rather than a proof of the backend.

technique 2: certificate-rejection testing and repair

Use this for credible compilation where an optimizer is allowed to be wrong but a checker must reject unsound certificates. The paper identifies three rejection causes: unsound transform, incorrect certificate, and an overly tight checker (Section IV-B, p.6). It states: “The script uses three random test-generation variants, run in sequence so that each variant tests the compiler as repaired by the previous variant.” (Section IV-B, p.6) The procedure is:

  1. Run the optimization sequence on generated programs; retain each checker rejection with pass name, rejection reason, and a trigger program (Section IV-B, p.6).
  2. Use three generators in sequence: T3a Csmith-style typed random programs; T3b skeletal-program-enumeration variants that scramble same-typed dataflow (six variants per seed); and T3c EMI variants that delete dead code, insert/delete in dead regions, or insert guarded live-region code (Section IV-B, p.6).
  3. Ask the repair agent to reproduce the trigger, decide whether transform, certificate generator, or checker is wrong, audit all consuming proof/code sites, make the minimal targeted repair, and validate on the trigger plus generated programs while preserving headline theorems (Section IV-B, p.6).

T3a found 21 distinct pass/property combinations in its first detect round; the campaign repaired 13 listed defects, including checker normalization oscillation, dead-edge handling, divide-dividend checking, unreachable-point obligations, register allocation, and simplifier omissions (Table II, p.8). The paper gives concrete fixes: skip a branch path proved dead; accept a moved dividend when the divisor is preserved; compute reachability before checking obligations; and recurse into comparison operands. T3b found one DAEobservable defect and repaired it with +2/−0 defect and +28/−22 proof lines (Table III, p.9).

Inference: A Verus analogue is a verified transform plus a certificate datatype and a proof fn checker whose ensures establishes refinement. The agent may edit executable transform code and proof lemmas, but a checker relaxation must be accompanied by a re-proved soundness lemma. Do not represent ensures on a spec fn or call a proof function at runtime.

technique 3: parser/printer round-trip testing

Use this for unverified text interfaces. Generate typed AST programs, print to text, parse back, and compare AST equality; this targets consistency, not malformed-input-only parser bugs (Section IV-C, p.6). Deduplicate records by seed/error and cap each error class at 20. The repair prompt groups records by root cause, audits parser/printer code, repairs, then reruns the original and new batches. The first phase processed 13,770,000 programs and all initially failed at the first declaration; four repairs (parser and printer) enabled a second phase of 18,075,000 programs with no defects (Section V-D, p.10; Table IV).

Inference: For Verus, specify a round-trip relation in a spec fn and use Rust property tests to exercise it; prove only the pure AST relation, while treating parser libraries and assembler behavior as trusted test targets.

evidence, limits, and product threat

The experiments used Claude Code Opus 4.8, Lean 4.28.0, an M4 Pro (12 cores, 24 GB), and agent-generated scripts; dollar costs were computed from published token rates, not invoices (Section V-A, p.7). The paper reports every detected defect/rejection repaired and no evidence of systematic reward hacking, but notes scripts and measurements were themselves agent-generated. It explicitly states that results concern compilers and may not generalize to less studied systems (Section VI, p.11).

Inference: For VL, ACDC is a high-value operational pattern: combine proof artifacts with randomized semantic differential tests, preserve seeds, and require repair validation on fresh inputs. It does not remove trust in Verus, the specification, model fidelity, or test-oracle completeness. VL should not redo generic Csmith/EMI ideas; the reusable contribution is their certificate-aware targeting and proof-update loop.

techniques for the catalog

  • certificate-aware differential execution — compare executable machine semantics with printed-and-executed code and retain reproducible seeds
  • credible-compilation rejection repair — classify certificate failures, localize transform/generator/checker causes, and re-prove checker changes
  • typed AST round trips — print and parse generated ASTs, compare equality, and repair parser/printer mismatches Checked 2026-10-13: audit record rinard2026automated; paper-study comparison complete; gate executed; experiments not rerun

Last edited: