PLDI 2026 (series) / PAgE 2026 (series) / PAgE 2026 / Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude CodeRemote
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.
Mon 15 JunDisplayed time zone: Mountain Time (US & Canada) change
Mon 15 Jun
Displayed time zone: Mountain Time (US & Canada) change
10:40 - 12:20 | |||
10:40 20mTalk | Agentic Code Reasoning PAgE Pre-print | ||
11:00 20mTalk | Towards Verified Code Reasoning by LLMs PAgE Meghana Aparna Sistla Google DeepMind, Gogul Balakrishnan Google, Patrick Rondon Google, José Pablo Cambronero Google, USA, Michele Tufano Google, Satish Chandra Meta Platforms, Inc. | ||
11:20 20mTalk | Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude CodeRemote PAgE Martin C. Rinard Massachusetts Institute of Technology | ||
11:40 20mTalk | The Next Frontier for AI-Generated Kernels: Correctness PAgE DOI Pre-print | ||
12:00 20mTalk | Testing LLM-Generated Distributed Protocol Code PAgE | ||