Paper: Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code

John R Levine <johnl@taugh.com>
Tue, 05 May 2026 20:57:12 -0400

          From comp.compilers
Related articles
Paper: Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code johnl@taugh.com (John R Levine) (2026-05-05)
| List of all articles for this month |
From: John R Levine <johnl@taugh.com>
Newsgroups: comp.compilers
Date: Tue, 05 May 2026 20:57:12 -0400
Organization: Compilers Central
Injection-Info: gal.iecc.com; posting-host="news.iecc.com:2001:470:1f07:1126:0:676f:7373:6970"; logging-data="75877"; mail-complaints-to="abuse@iecc.com"
Keywords: paper, tools
Posted-Date: 05 May 2026 20:57:34 EDT

The claim that the AI written proofs mean they don't have to test anything
seems a wee bit aggressive, but it's an interesting paper


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.


https://arxiv.org/abs/2605.01660


Regards,
John Levine, johnl@taugh.com, Taughannock Networks, Trumansburg NY
Please consider the environment before reading this e-mail. https://jl.ly

Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.