Devcon Archive logo
Devcon Devconnect Forum Blog
  • Watch
  • Event
    Event: background logo
    • Devcon 7
    • Devcon 6
    • Devcon 5
    • Devcon 4
    • Devcon 3
    • Devcon 2
    • Devcon 1
    • Devcon 0
    • Devconnect ARG
  • Categories
    Categories: background logo
    • Cryptoeconomics
    • Devcon
    • Developer Experience
    • Coordination
    • Core Protocol
    • Layer 2s
    • Real World Ethereum
    • Cypherpunk & Privacy
    • Security
    • Applied Cryptography
    • Usability
  • Playlists

Suggested

Loading results..

View all

About Devcon —

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.

An intensive introduction for new Ethereum explorers, a global family reunion for those already a part of our ecosystem, and a source of energy and creativity for all.

  • Watch
  • Devcon
  • Devconnect
  • Forum
  • Blog

Get in touch

devcon@ethereum.org

Subscribe to our newsletter

Crafted with passion ❤️ at the Ethereum Foundation

© 2026 — Ethereum Foundation. All Rights Reserved.

devcon8 / from production rust to lean 4 proofs a verification pipeline with ai provers

  • YouTube
From Production Rust to Lean 4 Proofs: A Verification Pipeline with AI Provers preview
  • Details

From Production Rust to Lean 4 Proofs: A Verification Pipeline with AI Provers

Duration: NaN:NaN:NaN

Speaker: Natalia Klaus

Type: Talk

Expertise: Some familiarity with the topic

Event: Devcon

Date: Nov 2026

A working pipeline from production Rust cryptographic code to kernel-checked Lean 4 proofs, built within the Ethereum Foundation's zkEVM Verification Project. Charon lowers Rust to a typed IR, Aeneas translates it to pure-functional Lean 4, and we prove the extracted code against formal specs from ArkLib and CompPoly. Closed so far: the arity-2 FRI fold step in Plonky3 matches a pure spec, never panics, no overflow (0 sorry). Also FRI round scheduling, Mersenne31 and KoalaBear field arithmetic, RISC Zero Merkle inclusion, 32-bit ADC via bv_decide. Two polynomial-algebra theorems connecting to ArkLib's foldNth remain open, and we show why they are hard. Running example: Aleph authored proofs of two bounds theorems that stood as sorry. Every AI proof is re-checked by the Lean kernel, so soundness never depends on the AI. We cover where AI provers help, where they fail, and the toolchain friction to budget for. Code: github.com/Verified-zkEVM/rust-lean. Preprint: arXiv:2605.30106.

Categories

ZKAIFormal Verification