Derek retweeted
The bull case for formal verification is "Here is a reusable library of properties/specs you can import in your code" not "Here is a few million LOC of Lean for you to go over, but the model passes!"
29
22
292
21,466
Derek retweeted
you've been using formal verification for ages and it's called using a language with a type system
21
18
341
9,799
Derek retweeted
A super cool use case for EthLib just unlocked!
With all the recent progress and the growing enthusiasm from new contributors, there's so much more to come!
With all the recent progress and the growing enthusiasm from new contributors, there's so much more to come!
Case in point as to why Ethlib is so cool. After patching up some holes in EthLib upstream, It finally can be used to formally verify smart contracts directly from the bytecode (here is a formal verification of USDT with nothing but lean4 + EthLib as an import):
github.com/Giulio2002/usd…
not only that, if you become more creative you can formally verify entire production clients (with this with enough agent time obviously)
2
4
22
1,155
Derek retweeted
Expanding on why I believe "ETH as store of value (SoV)" makes much more sense to focus on than "ETH as fee-burning token".
Three primary reasons:
1. ETH as fee-burning token never was as strong as it seemed
2. Optimizing for ETH as fee-burning token would demand Ethereum and ETH function in ways that are very hard to make compatible with decentralization and capture resistance.
3. Meanwhile, optimizing for ETH as SoV is aligned with Ethereum focusing on its unique strengths (decentralization and CROPS)
EIP-1559 (including its burn) is fine and good, we should keep them. But we should not feel sad if fee burn is < 10% of breakeven indefinitely; the value of ETH comes from elsewhere.
The core idea: the big thing that people appreciate about Ethereum is decentralization and CROPS. The main pragmatic benefit that these things translate into is stability. SoV is the category where that is not an unneeded extra we merely put effort into for ideological reasons, but rather a pragmatic strength from the perspective of people putting in their assets. And in the era of AI disruption, stability will be highly valued.
Three primary reasons:
1. ETH as fee-burning token never was as strong as it seemed
2. Optimizing for ETH as fee-burning token would demand Ethereum and ETH function in ways that are very hard to make compatible with decentralization and capture resistance.
3. Meanwhile, optimizing for ETH as SoV is aligned with Ethereum focusing on its unique strengths (decentralization and CROPS)
EIP-1559 (including its burn) is fine and good, we should keep them. But we should not feel sad if fee burn is < 10% of breakeven indefinitely; the value of ETH comes from elsewhere.
The core idea: the big thing that people appreciate about Ethereum is decentralization and CROPS. The main pragmatic benefit that these things translate into is stability. SoV is the category where that is not an unneeded extra we merely put effort into for ideological reasons, but rather a pragmatic strength from the perspective of people putting in their assets. And in the era of AI disruption, stability will be highly valued.
958
1,146
6,727
2,029,780
Derek retweeted
It's weekend guys, so it's time for some fun with the optimization of the quantum algorithms in ECDSA fail.
If you want to watch our duels, take a look at the webpage. New records coming! @odin_free @gopikannappan @JackieLeeETH
If you want to watch our duels, take a look at the webpage. New records coming! @odin_free @gopikannappan @JackieLeeETH
9
9
36
3,746
Derek retweeted
I'm giving a talk at Stanford tomorrow titled "Scaling Lean for AI."
Details here: beneficial-ai-foundation.github.io/SVIL2026_Fall/
Details here: beneficial-ai-foundation.github.io/SVIL2026_Fall/
8
37
260
12,346
Derek retweeted
We're very excited for 𝗦𝗼𝗳𝘁𝘄𝗮𝗿𝗲 𝗩𝗲𝗿𝗶𝗳𝗶𝗰𝗮𝘁𝗶𝗼𝗻 𝗶𝗻 𝗟𝗲𝗮𝗻 tomorrow! The in-person event is full, but livestream spots remain open: Register on Luma to receive the link: luma.com/kytl0zlj
𝗡𝗲𝘄𝗹𝘆 𝗮𝗱𝗱𝗲𝗱 𝘁𝗼 𝘁𝗵𝗲 𝗽𝗿𝗼𝗴𝗿𝗮𝗺: A closing round-table discussion on AI safety and formal verification (4:45–5:30 pm PT), moderated by Pedro Abreu (@p_droabreu0), host of the Type Theory Forall podcast, featuring Max Tegmark, Leonardo de Moura, Jonathan Protzenko, Andres Erbsen and Mike Dodds.
🔗 See the event website for the full program: beneficial-ai-foundation.github.io/SVIL2026_Fall/
𝗡𝗲𝘄𝗹𝘆 𝗮𝗱𝗱𝗲𝗱 𝘁𝗼 𝘁𝗵𝗲 𝗽𝗿𝗼𝗴𝗿𝗮𝗺: A closing round-table discussion on AI safety and formal verification (4:45–5:30 pm PT), moderated by Pedro Abreu (@p_droabreu0), host of the Type Theory Forall podcast, featuring Max Tegmark, Leonardo de Moura, Jonathan Protzenko, Andres Erbsen and Mike Dodds.
🔗 See the event website for the full program: beneficial-ai-foundation.github.io/SVIL2026_Fall/
Software Verification in Lean (SVIL) comes to Stanford University on Saturday, November 7.
Co-organized by Beneficial AI Foundation and Lean FRO, it is a day of public lectures on advancing Lean’s software verification ecosystem toward production use, with a focus on end-to-end y-critical systems.
Talks will cover Rust verification with the Aeneas framework, low-level software verification, and formally verified OS kernels.
Speakers include Max Tegmark, Shaowei Lin, Leonardo de Moura, Jonathan Protzenko, Andres Erbsen, and Mike Dodds.
In-person space is limited. Non-local and waitlisted registrants will receive a livestream link, and recordings will be available afterward.
Program and registration: beneficial-ai-foundation.github.io/SVIL2026_Fall/
9
25
218
15,746
Derek retweeted
We're ready to share our next verification pipeline!
Meet KEQ, a semantic equivalence prover based on the K Framework.
AI is getting good at rewriting legacy code, but the new version has to behave exactly like the old one (bugs included).
Tests can only show the presence of bugs, but not their absence. KEQ proves that two programs written in different languages match on every input, or it gives you a concrete counterexample.
Our first real-world trial has been proving equivalence between SHA 256 Rust and C implementations.
For more on how KEQ works, what's next, and how we're thinking of solving large-impact verification challenges, check out our latest blog post below.
A special thanks to the @Code_Metal_AI formal methods team, which inspired this work.
runtimeverification.com/blog/semantic-…
Meet KEQ, a semantic equivalence prover based on the K Framework.
AI is getting good at rewriting legacy code, but the new version has to behave exactly like the old one (bugs included).
Tests can only show the presence of bugs, but not their absence. KEQ proves that two programs written in different languages match on every input, or it gives you a concrete counterexample.
Our first real-world trial has been proving equivalence between SHA 256 Rust and C implementations.
For more on how KEQ works, what's next, and how we're thinking of solving large-impact verification challenges, check out our latest blog post below.
A special thanks to the @Code_Metal_AI formal methods team, which inspired this work.
runtimeverification.com/blog/semantic-…
7
15
55
2,664
Derek retweeted
and this is what you can build in a day when the math underneath has a high quality formalization
We shared our formalization of Stacks. Is it reusable?
The true test of a foundational library is what you can build on it.
Now, we release the Lean formalization of the proof of the renowned Weil conjectures (I-IV), one of which gives Riemann Hypothesis over finite fields. ✨
3
3
30
2,285
Derek retweeted
Mission 2028 puts formal verification at its core!
EthLib is a central part of this effort, and we've already made tremendous progress.
We need more eyes, more contributors, and more agents to help push this massive effort forward!
github.com/ethereum/EthLib
EthLib is a central part of this effort, and we've already made tremendous progress.
We need more eyes, more contributors, and more agents to help push this massive effort forward!
github.com/ethereum/EthLib
6
13
87
2,875
Derek retweeted
Join me at #Devcon8 for a session on Formal Verification of Consensus Protocols in Lean!
We'll explore how to correctly model and specify distributed protocols to formally prove their correctness.
Looking forward to seeing you there!
app.devcon.org/schedule/forma…
We'll explore how to correctly model and specify distributed protocols to formally prove their correctness.
Looking forward to seeing you there!
app.devcon.org/schedule/forma…
2
6
45
978