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.

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

Last edited: