fawad haider

Many people have claimed that with AI-assisted bug finding, secure code (and hence trustless anything) will be impossible. I have a much more optimistic take, and AI-assisted formal verification is a major part of the reason why: vitalik.eth.limo/general/2026/0…

@leonardoalt @leanprover Who writes the specs? Do you validate/review the specs carefully?

We can now fully rewrite most software in @leanprover and prove it correct: - Compiler module rewrite (AI) from Rust to Lean - Full FFI integration - All unit and integration tests pass - Formal spec and proofs!! - Under 20h wall time (unnoticed pauses) github.com/powdr-labs/cru…

And say if the Lean proof is too big/long to verify then we wrap it up in groth16 proof to say it exists :)

@QuangVDao hmmm interesting, haven't heard that direction yet, like hax/aeneas in reverse? that would require another tool which itself needs to be verified, no? or may be you are referring to Boole, upcoming framework in CSlib?

@BowlOfChilli sorry for the slow reply I think this is an interesting direction but not the most pressing one. It's probably more important to verify the correctness of efficient provers in Lean - would be nice if we can prove in Lean then emit code for both CPU & GPU

Our newest sum-check optimizations are out! eprint.iacr.org/2026/762 We propose a *better* domain for sum-check: the infinity hypercube. Evaluations over this domain give *precisely* the monomial coefficients, and lead to a ~10% prover speedup over 128+ bits prime fields 🧵/ n

@pirapira so do you let LLM write the specification too? The specification is where I imagine all issues popping up in lean "proven" code.

post: blog.zksecurity.xyz/posts/end-codi…

I wrote a blog post: the Final Form of Software Development. Why the assembly + Lean is final in both in the historical and category theoretic sense.

@rvtond @MistralAI Claude and homegrown are comparable? That’s very interesting. Can I ask about the homegrown solution?

@BowlOfChilli @MistralAI did not have great traction with vibe/leanstral -> ran into the 180K context limit and then compaction which diluted the task. combination of harness/model issues claude and homegrown succeeded. there are levers where homegrown is faster

pitting @MistralAI Leanstral against claude against homegrown agent, let's go

@dhsorens always confused by lean is implemented in lean, would love more of an explanation on this @Leonard41111588. Second there is a C/C++ compiler in the pipeline which generates machine code right and that is not formally verified?

another subtle and important point for practitioners, especially if extending Lean’s elaborator

A lil ambitious but directionally correct.

Doesn't this mean that all the world's code needs to be rewritten (and verified) in Lean @leanprover, ASAP??

@Leonard41111588 Great contribution. What happens to the current millions of lines of code(in mathlib etc ) in 2-3 years? Constant rewrite ?

Whenever I give a talk, people ask me: "What makes Lean different?", "Why did it succeed?" I finally wrote it down. Four things I believe, one honest weakness, and why "I fucking love this shit" keeps happening. leodemoura.github.io/blog/2026-4-2-…

@dhsorens Link doesn't work. Seems like an interesting talk

This was streamed! youtube.com/watch?v=yTru9F…

@royvanrijn @Leonard41111588 Oh just seeing this, didn’t know an open source model existed just for lean. This is very very cool. But curious what’s the business model here then?

@Leonard41111588 Thoughts on Leanstral? 😅 LLM 🤝🏻 Lean mistral.ai/news/leanstral

Prover correctness is becoming a central question as AI enters mathematics and software verification. New essay on why Lean's architecture is designed to survive AI pressure. leodemoura.github.io/blog/2026-3-16…

Just a few years ago, combining AI and formal mathematics was science fiction. Now it's happening. Interview with @ETAPSconf on Lean, AI, and why formal methods have never mattered more. etaps.org/blog/043-leo-d…

@rvtond With some caveats right? rust might be good but any language without the borrow checker might be hard to verify. C/C++/GPU kernels might be hard. But yes more and more Formal Verification will replace tests.

New post. Tests will be pointless. rijnard.com/blog/dear-agen…

@tcoratger This deserves some unpacking…are we going to formally verify the new lean spec before we implement in rust etc? And also say more about tests, not sure they are pointless for stateful changes, no?

Intersection between AI and formal verification is top of mind for me in the context of ethereum lean consensus specification!

@zksecurityXYZ @HarmonicMath @nico_mnbl @pirapira Nice, congrats!

We formalized FRI soundness in Lean, using @HarmonicMath and Claude Code. - FRI analysis by @nico_mnbl and collaborators - turned into a Lean proof by @pirapira 🔥

@drakefjustin @tcoratger whoa congrats @tcoratger

Today marks an inflection in the Ethereum Foundation's long-term quantum strategy. We've formed a new Post Quantum (PQ) team, led by the brilliant Thomas Coratger (@tcoratger). Joining him is Emile, one of the world-class talents behind leanVM. leanVM is the cryptographic cornerstone of our entire post-quantum strategy. After years of quiet R&D, EF management has officially declared PQ security a top strategic priority. Our journey began in 2019, with the "Eth3.0 Quantum Security" presentation at StarkWare Sessions. Since 2024, PQ has been central to the @leanEthereum vision. The pace of PQ engineering breakthroughs since then has been nothing short of phenomenal. It's now 2026, timelines are accelerating. Time to go full PQ: → PQ ACD: Antonio Sanso (@asanso) kicks off a bi-weekly All Core Devs PQ transactions breakout call next month. These sessions focus on user-facing security, covering dedicated precompiles, account abstraction, and longer-term transaction signature aggregation with leanVM. → PQ foundations: Today we are announcing a $1M Poseidon Prize to harden the Poseidon hash function. We are betting big on hash-based cryptography to enjoy the strongest and leanest cryptographic foundations. Check out our other $1M PQ initiative, the Proximity Prize. → PQ devnets: Multi-client PQ consensus devnets are live! Shoutout to pioneers @zeamETH, @ReamLabs, @PierTwo_com, @geanclient, @ethlambda_lean, as well as established consensus teams Lighthouse, Grandine, and soon Prysm. This incredible teamwork is coordinated by @corcoranwill via weekly PQ interop calls. → PQ workshops: Building on last year's PQ workshop in Cambridge (see photo), the EF is hosting another 3-day PQ event in October. Top experts from around the world will convene. In addition, a PQ day is set for March 29 in Cannes just ahead of EthCC. → PQ FV and AI: Last week Alex Hicks (@alexanderlhicks) ran a specialised maths AI for 8 hours, at a $200 cost. It one-shotted a formal proof one of the hardest lemmas in the foundations of hash-based snarks. Mind-blowing. Applied cryptography will never be the same. → PQ roadmap: A comprehensive breakdown of the EF's proposed PQ strategy will be shared soon™ on pq[.]ethereum[.]org. The roadmap targets a full transition in coming years with zero loss of funds and zero downtime. Stay tuned :) → PQ education: The ZKPodcast (@zeroknowledgefm) is producing a 6-part video series on Ethereum's PQ strategy. EF Enterprise Acceleration is also preparing material for enterprises and nation-states. Finally, Ethereum is now represented on the PQ advisory board that Coinbase announced yesterday. Believe in something. Believe in PQ security.

@public_dev_ A little simpler please :) are you saying a less than honest prover can make an initial big error appear smaller as we go through different sumchecks? I was trying to understand if GKR allows something more than a sumcheck itself allows for prover strategies.

@BowlOfChilli and what i'm thinking is: make a mock hostile prover can benchmark the mock value of some measurement...?? i think it might be hard, let's further talk about it!

Implementation of eprint.iacr.org/2025/2152.pdf with IEEE 754 floating point sumcheck gkr! github.com/indextree/gkr-… with forked version of soowon's gkr