Groups | Search | Server Info | Login | Register
Groups > comp.compilers > #3731
| Path | csiph.com!weretis.net!feeder9.news.weretis.net!news.misty.com!news.iecc.com!.POSTED.news.iecc.com!nerds-end |
|---|---|
| From | John R Levine <johnl@taugh.com> |
| Newsgroups | comp.compilers |
| Subject | Paper: Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code |
| Date | Tue, 05 May 2026 20:57:12 -0400 |
| Organization | Compilers Central |
| Sender | johnl%iecc.com |
| Approved | comp.compilers@iecc.com |
| Message-ID | <26-05-001@comp.compilers> (permalink) |
| MIME-Version | 1.0 |
| Content-Type | text/plain; charset="UTF-8" |
| 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 |
| X-submission-address | compilers@iecc.com |
| X-moderator-address | compilers-request@iecc.com |
| X-FAQ-and-archives | http://compilers.iecc.com |
| Xref | csiph.com comp.compilers:3731 |
Show key headers only | View raw
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
Back to comp.compilers | Previous | Find similar
Paper: Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code John R Levine <johnl@taugh.com> - 2026-05-05 20:57 -0400
csiph-web