Proof-Carrying Code For the Age of AI: Machine-Checked Guarantees from(…)
summary
Claims a practical pipeline: a Lean framework called EquiVM proves that deployed EVM bytecode refines a high‑level spec, and LLM agents autonomously complete refinement proofs for 23 contracts including MakerDAO. Proof artifacts reach ~84k lines; the largest end‑to‑end generation run takes ~100 hours while linking/checking can be ~20 minutes. Generation costs range from hundreds to thousands of dollars (one benchmark ≈ $1,400; MakerDAO suite ≈ $8,600). Results mostly succeed but require audited specs, a trusted Lean kernel, and engineering tradeoffs like native evaluation.
AI-written summary · about
chapters (40)
- 0:00Introduction
- 1:06Talk overview
- 2:30Declarative programming limits
- 4:57Need for machine-checkable correctness
- 6:44Proof assistants history
- 7:25Machines writing proofs
- 8:06LLMs novel compiler proofs
- 10:59MSR case studies
- 12:46Agent proving progress
- 14:09Proof-Carrying Code relevance
- 15:54Foundational PCC trusted base
- 16:56Source vs executable gap
- 17:37Refinement proofs compilers
- 19:27Per-artifact refinement proofs
- 21:17LLMs generate EVM proofs?
- 22:23Why EVM fits refinement
- 24:10EVM primer basics
- 30:30EVM bytecode refinement
- 35:50Soul Miner semantics
- 37:58Low-level refinement theorem
- 40:30Experiment autonomous proofs
- 43:20Benchmark results
- 48:59Correctness as artifact property
- 49:20Trusted base pitfalls
- 51:29Why not possible before
- 53:17Specification auditing challenges
- 54:22Proof checker auditing needs
- 55:28Open questions closing
- 56:52Q&A
- 57:14EVM semantics scalability
- 58:21Scalability costs repair
- 1:00:33Auditing specifications
- 1:02:39Prompt strategies workflow
- 1:03:40Spec vs executable comparison
- 1:05:26Proof writing bottleneck shift
- 1:07:12Technique effectiveness
- 1:09:01Proof bottleneck implications
- 1:10:06Infrastructure redesign
- 1:14:26Proof generation patterns
- 1:16:13Prompt engineering challenges
related talks
57mVerification, Cost, and Speed: What's Next for AI Coding at Scale
32mCan We Trust AI-Generated Code?
01h 01mDiscussion
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
21mEnhancing Symbolic Execution with Machine-Checked Safety Proofs
17mMakerDAO Smart Contract Safety - When Billions are at Stake
30mPractical Zero Knowledge Proofs
48mThe Proof Must Go On: Formal Methods in the Theater of Secure Software Development(…)