Proofs @Rise_MSR, @MSFTResearch. Compilers, Formal Verification, Cryptography. Previous: @Penn, @Bridgewater, @MIT.
Seattle, WA
Joined August 2009
- Tweets651
- Following1.2K
- Followers1.3K
- Likes2.7K
Pinned Tweet
🎉 Our paper “Structural Temporal Logic for Mechanized Program Verification” was accepted at OOPSLA 2025! We introduce Ticl, a program logic for compositional temporal proofs, beyond partial correctness, and directly over program syntax. #OOPSLA #Ticl
📄 arxiv.org/abs/2410.14906
This is a great start! The property “program does not crash” is useful, but not everything. Another useful property is “program does not spin” which we call liveness. Working to see if we can extend the Anthropic Linux model to liveness proofs.
New on our Frontier Red Team blog: using Claude to formally verify software at large scale.
Formal verification can prove that code is free of certain bugs, but historically it has only been feasible for small codebases (or required a lot of expert time).
With AI models, however, this is beginning to change. In collaboration with @theoremlabs, we used Claude to prove security properties in over one hundred real-world open-source libraries over the span of a few weeks.
Read our research in full here: anthropic.com/research/forma…
Lef retweeted
Introducing Flint, @Recursive_SI’s first model: a fast local coding model built with our automated research system, the Eureka Machine.
• Best-in-class fast local coding
• Up to 2x faster than comparable models: 125+ tokens/sec on a MacBook Pro, 150+ on RTX Spark
• Built from scratch in under 4 months
Private, unmetered intelligence on your own machine. Open weights available now on @huggingface, run it locally on your favorite framework or try it for free on @opencode or @pidotdev.
Lef retweeted
I've never trusted code I didn't review until now.
Agents write more code than any of us can review. We often end up skimming the PR/diff and pushing. Current review methods do not prove the code is correct or does what we asked. Recent research found the best AI code reviewer caught the bug on its first try only 42% of the time.*
The evaluation bottleneck, regressions, and security incidents have forced us to find a better way.
Introducing Proof-Driven Development Kit (PDD Kit) from @MSFTResearch. PDD Kit brings assurance to AI-generated code. You describe what you want to build in plain English. PDD Kit captures your objective, what we call your intent, and uses a verifier tool to prove the code meets it for every possible input.
You never review a single line of the code or the proof. You review your plan and the defined objectives in natural language.
A simple example is login. With testing, you check that only the correct password logs in a user but with a proof on top you can verify that there is no case a wrong password allows login. You can prove correctness and security across many complex scenarios.
Not only does PDD Kit prove the correctness of your code, but also your intent so you can have confidence your code is correct and does what you asked. It provides a level of assurance that specs, code review, and tests never could. PDD Kit is in limited research preview. Video explainer below.
If you want to learn more, I'll be sharing PDD Kit at GitHub Universe next week, Oct 28–29. Swing by the Speakeasy, ask for GitHub Next, and ask me about verified code. If you're in SF, let me know.
*Yang et al., "(When) Should a Software Factory be Lights-off?", Microsoft Research and CMU, Oct 2026
How do you _guarantee_ your agent's code is correct? You prove it.
Introducing Proof Driven Development Kit (PDD Kit) from @MSFTResearch.
PDD Kit helps turn your plan into a formal spec, then proves the agent's code meets that spec for every input. No vibe verification. PDD Kit is integrated with @GitHubNext's Chopin, so you can plan as a team.
PDD Kit takes an app's login flow from intent to a verified pull request:
It discusses your code, infers your intent as it goes, and proposes a formal spec in Verus, a proof language for Rust.
Once you approve the spec, the Verus verifier automatically proves the code meets it.
Where proof isn't possible, it falls back to empirical verification with tests and computer-use agents (CUAs).
It works on Rust today. No new language, no change in how you produce the underlying code, making formal methods more accessible.
The goal is a verified software factory, where engineers review specifications instead of code.
Come see it in action at GitHub Universe, Oct 28–29. Swing by the Speakeasy and ask for GitHub Next!
🚀 Zippel, our new programming language for #ZK proof systems, was accepted at S&P 2027! We used AI to write 20+ SOTA protocols, auto-verified them, and compiled to multithreaded #Rust that beats hand-written code on most benchmarks ⚡
📄 eprint.iacr.org/2026/2517.pd… #Cryptography
Lef retweeted
Neo in the Matrix, learns Kung-Fu without "training" by getting the skill uploaded to his brain.
Our new architecture, Spotlight, enables LLMs to grow and gain new capabilities without changing their weights. Check out our work!
1/ What would it take for LLMs to be able to grow their own capabilities?
We introduce spotlight, a memory architecture with growing capacity but with linear computational complexity. We show that this suffices to host evolving ecosystems like software by building Python directly into an LLM.
We also share some very early language modeling results where it outperforms attention and linear attention on long context capabilities!
Lef retweeted
how it feels listening to this podcast
Andrej Karpathy calls AI Agents slop
"Overall, the models they are not there. And I feel like the industry [...] it's making too big of a jump and it's trying to pretend that this is amazing.
And it's not—it's slop!
And I think they are not coming to terms with it. And maybe they are trying to fundraise or something like that, I'm not sure what's going on."
Lef retweeted
If you are at OOPSLA 2025, don't miss @elefthei's presentation of our paper "Structural temporal logic for mechanized program verification" on Saturday October 18, at 3:15 PM (Singapore time). Paper: arxiv.org/pdf/2410.14906. Code: github.com/vellvm/ticl.
Lef retweeted
I'm hiring at the EF: jobs.lever.co/ethereumfounda…
If you're into Ethereum, cryptography, and formal verification, please get in touch! 🙂
Lef retweeted
excited that my team at @Bloomberg is supporting PhD students in certified programming (and other infra/sec topics too!) through a fellowship. 💻🛡️
includes stipend, tuition, and internship. timely for Rocq and proof assistant folks as science funding tightens. please apply! 📬
#CFP: Applications for Bloomberg’s 2025-2026 #Infrastructure & #Security Ph.D. #Fellowship are now being accepted.
Submission Deadline: Friday, July 18, 2025 (11:59 PM AoE)
bloom.bg/3HLdfmO
#InfoSec #supplychainsecurity #ProgramAnalysis #BugFinding
Theory is saying a DAG does not have cycles. Engineering is still adding a “visited” vector to the worklist algorithm because you know you will eventually hit a bug and it’s gonna be a pain to debug an infinite loop.
People using SMT solvers don’t know you can simply implement algebraic simplifications with smart constructors in 5x the time.
An interpreter is simply dynamic dispatch on a loop. A compiler trades dynamic dispatch for static dispatch. Can we have the cake (an interpreter) and eat it too (static dispatch)?