Full verification of compiler optimizations requires roughly an order of magnitude more development effort than credible compilation when implemented by a coding agent.
Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
abstract
This paper presents the use of testing, credible compilation/translation validation, verification, and audits in the Axon compiler. Axon comes with fully machine checked proofs that guarantee the correctness of the generated code. All code and proofs were written in Lean by Claude Code, with the correctness proofs eliminating any need to audit or examine any verified code. I present a development process for using these validation techniques, evaluate the use of this process during the development of the compiler, and discuss implications for other development efforts.
citation-role summary
background 1
citation-polarity summary
fields
cs.PL 1years
2026 1verdicts
UNVERDICTED 1roles
background 1polarities
unclear 1representative citing papers
citing papers explorer
-
Quantitative Comparison of Credible Compilation and Verification In Coding Agent Compiler Development
Full verification of compiler optimizations requires roughly an order of magnitude more development effort than credible compilation when implemented by a coding agent.