research engineer | formal verification @ethereumfndn
- Tweets 998
- Following 1,595
- Followers 586
- Likes 10,017
for any of you crazy fuckers that want to experiment with LLMS-as-compilers, and write code directly in risc-v assembly (in Lean), we isolated the risc-v interpreter here that we use for evm-asm. open for contributions - please open issues with features or improvements you’d like to see! 🦾
github.com/Verified-zkEVM/ri…
6
6
61
4,017
Derek retweeted
AI is pushing the limits of software security, making Formal Verification (FV) essential for Ethereum's defense.
But FV doesn't magically secure everything.
In a new EthResearch post, @asn_d6 & @kevaundray explore the Trusted Computing Base (TCB). 🧵👇
1
3
23
956
Derek retweeted
stateless-pancaketh is a stateless guest of Ethereum in development. It's written in a programming language called Pancake.
2
2
5
799
Derek retweeted
A two-weekend fun project: Vermilion, an experimental Lean 4 backend for Verus verifier for Rust. Verification conditions are readable Lean theorems, provable with an SMT solver, Lean's grind, Mathlib lemmas, by hand, or by your favorite AI system.
github.com/ilyasergey/vermil…
6
20
169
7,364
Idk about this natural language only interaction. It can be very hard to know what you actually want, and often the best way to find it out is by articulating it yourself, precisely and rigorously (read: implementation or formal spec)
Formal Verification will very quickly reach its full potential as what it was meant to be from the beginning: a means to an end.
But not as it started. As it will end.
1. From human intent, AI will generate the code, the spec, and the proof, all together as bundle. Without the spec and proof, the code is just garbage and no human should even consider it.
2. The spec will be rendered back to the human in natural language as feedback, for approval. We will not see any code, spec, or proof. The rendered feedback will be as close it can be to the original intent, otherwise humans will not approve it.
3. The engine will generate an independently checkable proof that the loop has been closed, with a provably correct artifact that matches the human intent.
I call this Intent Computing. Where the AI is the new Computer and Intent is the new Programming Language.
1
4
359
Derek retweeted
Breakthrough result!
This closes the final gap to have lattice based SNARKs everywhere and for everything
LaBinius: Lattice-based Polynomial Commitment Scheme over a Binary Field.
Excited to present LaBinius, my recent work with @gregor_seiler.
We show how to instantiate an Ajtai commitment over extremely efficient cyclotomic power-of-three rings and then connect it with a polynomial opening mod 2, so that R/2R is a binary field.
Such a PCS is bridged with SOTA frontends, including Flock and Binius, to obtain end-to-end proofs of standard hashes with throughput of tens of thousands per second.
osdnk.me/blog/labinius
1
10
111
9,366
RT @yukonresearch: How one better.codes proof became four papers
- Aug 27. @nasqret pushes the better.codes bound fr…
15
1
Derek retweeted
Happy to announce my latest work with @skominers and @SuccinctJT !
eprint.iacr.org/2026/2056
TLDR: we transfer the techniques from better.codes to yield 5-10% proof size reductions in several SNARKs today, and supply an efficient decoder for knowledge soundness
🧵/ n
6
26
146
10,017
Derek retweeted
Bend 2 is here!
It is a new programming language that blocks AI mistakes via *proof checking* - the same technique big AI labs used to solve open math problems, like Navier-Stokes.
It is also very fast, and runs on GPUs.
Watch the video. Link in the comments.
RELEASE DAY
After almost 10 years of hard work, tireless research, and a dive deep into the kernels of computer science, I finally realized a dream: running a high-level language on GPUs. And I'm giving it to the world!
Bend compiles modern programming features, including:
- Lambdas with full closure support
- Unrestricted recursion and loops
- Fast object allocations of all kinds
- Folds, ADTs, continuations and much more
To HVM2, a new runtime capable of spreading that workload across 1000's of cores, in a thread-safe, low-overhead fashion. As a result, we finally have a true high-level language that runs natively on GPUs!
Here's a quick demo:
622
1,236
10,692
1,727,985
Derek retweeted
Fantastic progress on binary field techniques in Plonky3 lately.
We just opened a bunch of AArch64 performance issues if you want to dig in. The optimizations get quite subtle, so we highly recommend throwing your best LLM at them :)
github.com/Plonky3/Plonky3/i…
3
5
58
2,232
Derek retweeted
I'm excited to announce `waterfall`, a new Lean tactic for ACL2-style automated proof search.
It can automatically find proofs of the kind we do a lot in formal PL and software verification: lots of induction over data structures, case analysis, etc.
samth.github.io/waterfall/
9
19
198
8,412
Derek retweeted
Lean 4.34.0 is out: 159 changes. Three kernel soundness vulnerabilities fixed, all requiring deliberately constructed inputs rather than ordinary code. 𝚋𝚟_𝚍𝚎𝚌𝚒𝚍𝚎 is up to 6x faster. lean-lang.org/doc/reference/…
#LeanLang #LeanProver
6
38
249
7,735
Derek retweeted
The EF Protocol Cluster's 15th AMA begins in 24 hours
Ready to learn about Ethereum's potential futures?
Ask away!
→ Submit questions now: teddit.net/r/ethereum/commen…
→ Answers roll in on Sep 16 at 2pm UTC
The EF Protocol teams are hosting a Reddit AMA on September 16.
This is your chance to ask EF Protocol researchers and devs directly.
Submit your questions about post-quantum Ethereum, L1-zkEVM, formal verification, the future of state, finality, privacy, and more now!
🔗↓
8
15
88
8,899
Derek retweeted
We're happy to share that the @powdr_labs team has joined @axiommathai!
As we begin this next chapter, here's a look at some of the work that brought us here:
6
4
93
34,107
Derek retweeted
Welcome @powdr_labs to Axiom!
@powdr_labs has been rethinking the software stack from the bottom up around machine-checked correctness: from autoprecompiles for zkVMs to a ZK-native stack with crush + powdr-wasm.
We share this vision. Very excited to build together 🚀🚀🚀
We're happy to share that the @powdr_labs team has joined @axiommathai!
As we begin this next chapter, here's a look at some of the work that brought us here:
4
13
66
14,993
Derek retweeted
Built a little tutorial for how to get verified correct and FAST executable code out of Lean 👇
Thanks for the prompt @alinush!
Regarding doing stuff in "just Lean," (which would be great IMO: less languages => less tooling/complexity => less headache), I could not really find any meaningful tutorials.
e.g., I'm thinking "here's a sorting spec in Lean, a merge sort implemented in Lean that you can compile and run and a proof that it sorts according to the spec."
2
9
44
3,618
Derek retweeted
Performant formally verified software by @leonardoalt
One of the most interesting consequences of formal verification: you can optimize much more aggressively when every rewrite has to preserve a proof.
leoalt.de/performant-verifie…
1
12
66
2,721
Derek retweeted
Organizing open problems into batches which are solvable by similar methods. Alignment of AI is a big topic, better RL, designing new formal systems. There is not much left on a very classical technical level, we are in the endgame here. Also new kind of education.
1
8
376
Derek retweeted
Today, a certain era in mathematical benchmarks is coming to an end. We designed this set of tasks in the era of the o4-mini model and initially expected the pace of solving them to be rather slow. Things started getting serious in January, and I made a prediction back then that the benchmark would saturate within nine months. Even despite the invalidation of some incorrectly formulated tasks, that prediction turned out to be pretty accurate.
The part that gives me chills is that I still can't solve most of these problems myself, and probably never will. And, as FirstProof showed too, the chance of finding a problem for which we know the answer, yet which none of the vanilla or harnessed AI models can solve, is basically close to zero.
I think we need to completely change our understanding of what is actually hard in mathematics now. Maybe, after all, the only things left in the universe are black holes and Busy Beavers…
Every FrontierMath Tier 4 problem has now been solved by AI, with GPT-6 Astra solving the last problem standing. Mathematicians often commented that AI found unintended shortcuts when solving their Tier 4 problems. Not so for this last one, which was created by Jay Pantone.
17
49
433
27,268
A much-welcomed checker to root out any mysterious proofs of False in enormous autoformalisations
Lean has a new checker: con-leche, a CONsistent LEan CHEcker. This is an external checker for Lean that is proven (in Lean) to be consistent, meaning it does not accept a proof of False.
Joachim Breitner (@nomeata) is the mastermind behind the project. github.com/leanprover/con-le…
4
353