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…
5
184
🚀 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
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.
2
3
458
People using SMT solvers don’t know you can simply implement algebraic simplifications with smart constructors in 5x the time.
2
220
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)?
2
3
509
I used to think ASTs with just two constructors UnaryOp and BinOp where old fashioned, but I think it actually saves a ton of lines of code (especially if using copilot).
2
270
Post-dissertation proposal exhaustion and a new Churchill documentary dropped on Netflix? Say less!
5
254
reify . reflect
A lot of math is normal
ALT Knights point their swords to the centre of a round table. The swords are captions with v/||v||, a normal distribution, H normal subgroup of G, normal bundle, normal topological space, A*A=AA*, and a plane with it’s normal vector. The centre of the table is captioned “normal”.
1
336
