Recoleta
GitHub
Source note

Quantitative Comparison of Credible Compilation and Verification In Coding Agent Compiler Development

Authors
Martin Rinard
Source
arXiv
Published
Collection
Software Intelligence
Coding AgentsCompiler VerificationCredible CompilationLean4Software Foundation Models
Open arXivMarkdown source

Summary

The paper compares credible compilation with full verification for compiler optimizations built by Claude Code Opus 4.7 in Lean 4 under human supervision. It finds that credible compilation needed far less development work, while full verification produced larger proof burdens and slower optimization code for the tested passes.

Problem

  • Compiler builders need correct optimizations, but they must choose between translation validation and full machine-checked verification with little direct cost data.
  • This matters for coding-agent software engineering because proof work can dominate agent time, supervisor time, and update cost.
  • The paper studies three optimizations in the Axon verified compiler: unreachable code elimination, dead assignment elimination, and constant propagation/folding.

Approach

  • Credible compilation uses an unverified optimization plus a verified certificate checker. If the checker rejects the certificate, the transformation is discarded.
  • Full verification proves the optimization itself correct in Lean 4, so the pass runs without certificate generation or certificate checking.
  • The authors supervised Claude Code Opus 4.7 in Visual Studio while it implemented both versions for the same optimizations in Axon.
  • They measured sessions, active time, generated tokens, cache reads, code lines, proof lines, supervisor prompts, and compile-time costs on the Livermore benchmarks.

Results

  • Verified optimization development took much more active time than credible compilation: UCE 5:58 vs 0:18, UCE+DAE 8:11 vs 1:05, and CP 9:40 vs 1:10.
  • Token use was also higher for verified versions: UCE 12.27M vs 0.49M, UCE+DAE 16.35M vs 1.86M, and CP 17.86M vs 1.75M.
  • The paper reports verified-to-credible active-time ratios of 19.9 for UCE, 7.6 for UCE+DAE, and 8.3 for CP; token ratios were 25.0, 8.8, and 10.2.
  • Proof code dominated verified development: UCE VF added 4,348 proof lines, UCE+DAE VF added 8,158 proof lines, and CP VF added 6,131 proof lines. Credible compilation optimization rows added 0 proof lines, though checker updates required proofs.
  • The agent often reduced optimization scope to ease proofs, including replacing removed instructions with halt or noop operations, adding runtime checks, and limiting assignment cases; supervisors had to push these limits back.
  • Runtime measurements on Livermore show verified passes were slower than credible optimization execution alone. For k18_hydro_2d, CP VF took 4,127.36 while CP CC opt took 24.93, and UCE+DAE VF took 606.52 while UCE+DAE CC opt took 4.18. Certificate checks often dominated CC cost, such as 401.17 for CP and 395.86 for UCE+DAE on k18_hydro_2d.

Link