@fbinfer @rescriptlang Hanging out with @magnesCH
Joined June 2011
- Tweets1.4K
- Following122
- Followers1.3K
- Likes4K
Building TScert means modeling the libraries it calls, and checking each model against the real implementation, not its type declarations.
The declarations are often imprecise, sometimes wrong. `crypto.fips` is declared boolean; Node returns 0. `import.meta.dirname` is declared string; it's undefined outside file: modules. It also rediscovered a confirmed TypeScript bug: the compiler API panics on the type of `c ? s : []`.
Building TScert: TypeScript based on a formally verified core, one feature at a time.
@typescript made smart, pragmatic tradeoffs on a very hard problem. With unlimited agents, those tradeoffs can be revisited.
First milestone: TScert verifying its own front end, which uses the TypeScript compiler's libraries.
189 functions out of 499 verified so far.
That compiler API panic, across TypeScript versions:
• TS 6 (JS): never had it
• TS 7.0.2 (Go): panics, the call throws
• TS 7 main: fixed (#64080)
• Rust port of the Go code: same panic, same message, until it ported the fix
• C++ port: no public code
Perhaps the bitter lesson was successful as back then it was a contrarian position.
The contrarian position now is to completely ignore it.
Cristiano Calcagno retweeted
Lean Verified Tokenizers (srush.github.io/verified-tok…)
Training-inference mismatch kills RL runs, but yet we build messages in Jinja? Prototypes a Lean-verified Rust agent pipeline.
Cristiano Calcagno retweeted
The strong exponential time hypothesis (SETH) explained by MIT professor @rrwilliams who was selected by OpenAI to verify the recent breakthrough result:
Q: "Could you explain the Strong Exponential Time Hypothesis, or SETH, and its significance?"
Ryan Williams: "Strong ETH is a severe strengthening of the P versus NP question. P versus NP is asking whether the SAT problem has a polynomial-time algorithm or not.
Strong ETH is basically saying that for the SAT problem, you cannot solve it much faster than 2^n. There’s no 1.999^n time algorithm. For every string of 9s, there is no 1.9999^n time algorithm. To say it totally precisely, it has to do with the k-SAT problem, where you’re looking at clauses of length k for arbitrary k, but those details don’t matter so much.
SAT is a canonical NP-complete problem. It’s solved all the time in practice. It’s extremely useful for verification; nowadays it’s an engine for verification. So it can be solved fairly well in practice. However, in the worst case, we still don’t know how to solve it significantly faster than 2^n.
So the hypothesis that it needs, say, 1.99999^n time is a very strong exponential time hypothesis. It’s stronger than P versus NP. It says it’s not just superpolynomial. It’s darn near 2^n time that you need."
Q: "Do you think that hypothesis is true? Why or why not?"
Ryan Williams: "I think I’m on the record as not believing this hypothesis.
Why don’t I believe it? I started thinking about this hypothesis maybe already as an undergrad, but certainly early in grad school. Before it was even called Strong ETH, I guess that shows how old I am. I was trying to figure out how to solve CNF-SAT faster than 2^n.
At the time there were a number of other NP-complete problems that had faster algorithms, like subset sum. So I thought, what’s so special about SAT? If all these other problems have faster algorithms, why not SAT as well?
Even 3-SAT, where each clause is an OR of 3 variables, has a faster algorithm, and this is just a more general version of SAT. So at first I thought there’s no good reason to believe a lower bound. These other related problems have upper bounds, so why not?
But then, over time, I would have different attacks on Strong ETH, always trying to refute it in different ways. These attacks would fail in some completely catastrophic and ridiculous way. They would have no chance of actually solving the original problem.
But by staring at my failure, I’d think: there’s something interesting happening here. It doesn’t refute Strong ETH, so what does it do? By trying to pivot and figure out what I could do with my failure, I was able to solve a variety of other problems instead.
So after a while, I realized that the truth value of Strong ETH to me is almost irrelevant. If I believe that it’s false, then I get good ideas.
By thinking about what an algorithm that breaks 2^n could look like, I force myself to think in a different way. I have to discard the natural algorithmic possibilities, because we know they won’t work, and think in a different direction. Because it sends my brain in a different direction, it’s very useful for research. Even though I still haven’t refuted it, it’s very useful for me to believe that it’s false, operationally."
Q: This is a minority opinion, right?
Ryan Williams: "Russell Impagliazzo, a good friend of mine who helped propose this, always emphasizes to me: this is a hypothesis. We explicitly did not name it a conjecture. We wanted to put forth a lower bound that would get you to think about it, something a little more controversial than P versus NP or other things people more normally believe.
Hypotheses at the edge of our understanding, where we truly don’t know what the answer might be based on our intuition, can be enlightening to think about. That’s one reason why it was proposed.
But one reason you might believe Strong ETH is true is that it conveniently implies a lot of other lower bounds. You can reduce SAT to a bunch of problems that seem totally unrelated, like edit distance and various pattern matching problems. They have natural polynomial-time solutions. If you could improve on the algorithms for any of those, you would improve the one for SAT as well, and get something better than 2^n.
So believing in it makes a convenient worldview. It shows that all these different textbook algorithms are indeed optimal."
Announcing three major scientific discoveries, one each in mathematics (harmonic analysis), computer science (complexity theory), and physics (quantum field theory).
AI starting to help us improve our understanding of the universe! openai.com/index/building-sc…
Cristiano Calcagno retweeted
Overall, fuzzing and LLMs are complementary approaches. AI has greatly increased the number of vulnerabilities found and fixed in V8, but don’t turn off those fuzzers yet!
Building TScert: TypeScript based on a formally verified core, one feature at a time.
@typescript made smart, pragmatic tradeoffs on a very hard problem. With unlimited agents, those tradeoffs can be revisited.
First milestone: TScert verifying its own front end, which uses the TypeScript compiler's libraries.
189 functions out of 499 verified so far.
Cristiano Calcagno retweeted
We just sent out the last batch of invites for Vibecheck (fmxai.org/vibecheck). We're now at capacity (for the building, for two floors). The event is going to slap and I'm really, really excited about it!
- HUGE thanks to our sponsors, including @datadoghq , @theoremlabs , @omni, @workersio , @SafeWithAtlas, @astriolabs, For-All R&D (@qd_forall), and @thegp. This would be totally impossible without you!
- I'm also really stoked about several companies that are providing compute and platform tokens for competitors, including: @anthropicai, @PrimeIntellect, party.build, @lanyon_ai , @wearerandomlabs .
- And finally, we have some amazing experts who've helped plan the event and/or will be in attendance helping to run the event and judge entries, including folks from several of the above-mentioned companies, and from several academic labs, as well as from @mathematics_inc , @axiommathai , and @HarmonicMath .
I'll be sending rejection emails for anyone who didn't make it in shortly, and will close down the application form. If any currently RSVPd people cancel, we will send some last-minute invites accordingly. If you wanted to participate in this event but didn't make it in, please note two things: first, this does not reflect poorly on you -- we specifically aimed to accept people from a wide variety of backgrounds, not just a bunch of our friends or of FM experts. And second, we are going to run more of these events! We are loosely planning to run a London event, colocated with FMxAI London in 2027 (and co-organized with @galois, see fmxai.org for more ..); a NYC event, at some TBD date; potentially also an online/remote one; and a defense-oriented event co-organized with @mathematics_inc. If you're interested in one of these let me know.
This event is absolutely a labor of love, and we hope you'll follow along. We'll be posting updates, repos, podcast episodes, video interviews, and more throughout, and it's going to be a lot of fun. Also, if you didn't make it in but want to experiment in your free time, we will be posting all the rules and judging criteria in the coming weeks on fmxai.org/vibecheck, and we encourage you to play around and post your work!
And for those of you who got in, see you in SF!!
Cristiano Calcagno retweeted
Yes, I ran @opentaint, our static taint analyzer, on a mid-sized Java project (~100K lines, ~0.65 MB of bytecode), checking for the absence of path-traversal data flows. The numbers come from that run, though the estimates for AI and formal verification are speculative.
The problem with formally proving dataflow properties across a whole project is that you need abstract dataflow semantics for every method. AI can generate those, sure, but without proving them sound, you're just trusting whatever it came up with.
So let's assume we do it properly: embed JVM bytecode into a formal verifier, have AI generate field- and context-sensitive (but path-insensitive, for a fair comparison) semantics for each method, prove them sound, and then prove or disprove the security property. We can even assume the external library models and security rules are already there, so we don't count their cost.
For this one project and one property, the taint analyzer produced ~440 MB of dataflow summaries and fixpoint artifacts. Based on that, I estimate ~28.5B input tokens and ~145M output tokens for a cold AI-based formal verification run. That's around $11,500 at Opus 5.5 API prices. And this isn't just a one-time cost: at least some of that information would need to be recomputed whenever the codebase changes, though unchanged proofs could be reused.
Since these estimates are based on the bytecode size, method summaries, and fixpoint data from the taint analysis, actual costs could differ significantly depending on how much work the proof engine handles itself and how much can be reused. But the more work you offload to the proof engine, the closer you get to having it perform the static analysis itself. Anyway, take the numbers with a grain of salt.
Meanwhile, static taint analysis computes the same dataflow properties in minutes on a CPU, without any API token costs.
That's why, before rewriting a codebase in another language or spending tokens on AI agents proving dataflow properties, I'd suggest trying static taint analysis first.
It has its own problems, of course. Performance can vary widely between projects, and what works well in one can struggle in another. To me, a much more interesting direction is making these analyzers flexible and interactive enough that AI agents can tune them for a particular project, identify bottlenecks, and work around them, rather than pushing agents to do the whole analysis themselves
Cristiano Calcagno retweeted
yes, and the better language design using finite fields and other structures according to langsec.
Part of formal verification can be replaced by more efficient static analysis, and part of static analysis by better programming language design.
If you enjoy riding waves you might as well be early riding one of the next ones (accepting the risk that they won’t come).
Or slightly less oversimplified:
nitter.cf/alexlavaee/status/2114…
Don't learn formal methods.
Writing proofs by hand is what kept formal methods niche for over 75 years. seL4 took about 20 person-years to prove 8,700 lines of C. Agents take that part now. What's left for you is the spec, and knowing which language fits the job.
That's why the history matters. Formal methods means stating what a program or system must do in precise math, then using a tool to check that the code or design meets it. Here's how we got here, what each language is good for, and where I'd start.
FOUNDATIONS (1947 to 1979)
1947: Goldstine and von Neumann annotate program flow diagrams with "assertion boxes" stating what holds at each point.
1949: Alan Turing's "Checking a Large Routine" proves a short program correct using assertions. The idea mostly sits unused for over a decade.
1962: Carl Adam Petri's dissertation introduces Petri nets for modeling concurrent systems.
1963: John McCarthy, "A Basis for a Mathematical Theory of Computation".
1966-67: Peter Naur and Robert Floyd independently show how to prove programs with assertions attached to points in the code.
1967: N. G. de Bruijn starts Automath, the first language for computer-checked mathematical proofs.
1969: Tony Hoare publishes Hoare logic, {P} C {Q}. Nearly every contract language since builds on it.
1972: Robin Milner's Stanford LCF. Its Edinburgh successor (1979) introduces ML as its scripting language, the ancestor of Standard ML, OCaml and F#.
1973: Mizar starts in Poland. Formalized math that reads close to a textbook.
1975: Dijkstra's guarded commands and weakest preconditions.
1977: Amir Pnueli brings temporal logic to programs. Patrick and Radhia Cousot publish abstract interpretation, the theory behind sound static analyzers.
1978: Hoare's CSP for concurrent processes. Milner's CCS (1980) and the pi-calculus (1992) follow.
1970s: VDM at IBM's Vienna lab. Jean-Raymond Abrial proposes Z, later developed at Oxford. Boyer and Moore build their theorem prover.
TOOLS PEOPLE USED (1980 to 1999)
1981-82: Model checking, invented independently by Clarke and Emerson and by Queille and Sifakis. Turing Award in 2007.
1980s: Synchronous languages Esterel and Lustre in France. Lustre becomes SCADE, which Airbus uses to design flight control software.
1984: Nuprl at Cornell.
1985: Coquand and Huet's Calculus of Constructions, the logic under Coq.
1986: Isabelle (Larry Paulson).
Late 1980s: SPARK, a provable subset of Ada.
1988: HOL (Mike Gordon).
1989: Coq's first public release. Renamed Rocq in 2025.
1990: Symbolic model checking with BDDs handles 10^20 states. McMillan's SMV follows.
1991: SPIN model checker goes public (Gerard Holzmann, Bell Labs).
1992: PVS at SRI. Oxford and IBM win the Queen's Award for using Z on IBM's CICS transaction system.
1993: Metamath, a proof language simple enough to check with a few hundred lines of code.
1994: Lamport's TLA. TLA+ follows in 1999.
1994-95: Intel's Pentium division bug costs it $475 million. AMD uses ACL2, Kaufmann and Moore's successor to the Boyer-Moore prover, to prove its K5 floating-point division correct. Intel hires John Harrison in 1998 and uses his HOL Light to verify floating-point algorithms.
1996: Abrial's B-Book.
1997: Alloy (Daniel Jackson, MIT).
1998: Paris Metro line 14 opens driverless, with safety software built in the B method. The KeY project for Java verification starts.
1999: Agda (Catarina Coquand). JML, a contract language for Java.
VERIFIERS MEET REAL CODE (2000 to 2019)
2000: Microsoft's SLAM project starts. It ships as the Static Driver Verifier in the Windows driver kit.
2001-02: Separation logic (Reynolds, O'Hearn, Yang) makes pointer-heavy code provable.
2002: ESC/Java. Spec# (2004) and the Boogie verifier (2005) follow at Microsoft Research.
2003: Astrée proves the Airbus A340's primary flight control software free of run-time errors.
2004: CBMC, bounded model checking for C.
2005: Georges Gonthier finishes a Coq proof of the four color theorem.
2006: CompCert, a C compiler proved correct in Coq (Xavier Leroy). Event-B gets its Rodin toolset around the same time.
2007: Agda 2. Idris first appears (Edwin Brady).
2008: Z3 SMT solver (Microsoft Research). Frama-C. VeriFast.
2009: Dafny (Rustan Leino). seL4, the first general-purpose OS kernel with a machine-checked proof that its C code matches its spec.
2010: Why3.
2011: F*.
2012: A Coq proof of the Feit-Thompson odd order theorem is completed.
2013: Lean (Leonardo de Moura, Microsoft Research). P language at Microsoft.
2014: CakeML, a verified ML compiler. Liquid Haskell. Flyspeck finishes a formal proof of the Kepler conjecture.
2014-15: AWS reports TLA+ found bugs in S3 and DynamoDB that testing missed. IronFleet proves distributed systems correct in Dafny.
2015: Iris, a separation logic framework in Coq. Facebook open-sources Infer.
2016: Project Everest starts, aiming for a verified HTTPS stack. Viper.
2017: HACL*, verified crypto written in F*, ships in Firefox 57. Lean's mathlib starts.
2018: AWS Zelkova checks IAM and S3 policies with SMT solvers.
2019: Fiat Cryptography's Coq-generated code lands in BoringSSL, used by Chrome. Prusti for Rust.
LLMS MEET PROOF CHECKERS (2020 to 2025)
2020: OpenAI's GPT-f finds shorter Metamath proofs that get accepted into the main library, a first for deep learning.
2021: Lean 4.
2022: Kani (AWS) and Creusot for Rust. Aeneas translates Rust into Lean. The Liquid Tensor Experiment finishes the Lean proof Peter Scholze asked for.
2023: Verus for Rust. AWS releases Cedar, a policy language built with proofs in Dafny and later Lean. LeanDojo gives models a programmatic interface to Lean. Terence Tao's team formalizes the PFR conjecture proof in Lean in three weeks.
July 2024: DeepMind's AlphaProof reaches IMO silver-medal standard with proofs in Lean.
Sept 2024: Quint 1.0, TLA+ ideas with ordinary programming syntax.
Mar 2025: Imandra launches CodeLogician, an agent that turns code into its IML logic and checks it.
Apr 2025: AWS publishes how it rewrote its authorization engine, called a billion times per second, in Dafny with proofs.
July 2025: Harmonic's Aristotle reaches IMO gold-medal level with formal Lean proofs.
Sept 2025: The vericoding benchmark tests LLMs writing verified code from 12,504 specs. Off-the-shelf models pass 82% in Dafny, 44% in Verus, 27% in Lean.
LANGUAGES BUILT FOR AGENTS (2026)
Feb 22, 2026: Vera. "A programming language designed for LLMs to write, not humans."
Feb 25, 2026: Vow. "A Programming Language for Agentic Coding."
Mar 9, 2026: Kōdo. "Designed for AI agents to write." Z3-checked contracts, JSON errors with patches.
Sept 17, 2026: Bend 2. Dependent types and Lean-style proofs, C-like speed, CPU and GPU parallelism, Python-like syntax.
WHAT EACH LANGUAGE IS GOOD FOR
Specs and models
Z: precise requirements docs. Little tooling today.
VDM, B, Event-B: refining a spec step by step into code. Railways and safety-critical control.
CSP (with the FDR checker): concurrent protocols.
Petri nets: workflows and concurrent processes.
TLA+ and Quint: distributed system designs, consensus, race conditions before you write code. Checks the design, not the code.
Alloy: fast counterexamples in data models and access rules. Bounded, so finding no counterexample isn't a proof.
P: modeling and testing event-driven distributed services at AWS and Microsoft.
Model checkers
SPIN: concurrency protocols, as abstract models.
NuSMV and other SMV descendants: hardware and finite-state control logic.
CBMC: bounded checking of C code.
Kani: bounded checking of Rust, including unsafe code.
Static analysis
Astrée: proving embedded C has no run-time errors. Avionics.
Static Driver Verifier: Windows drivers using kernel APIs correctly.
Infer: memory and null bugs across large codebases.
Proof assistants
ACL2: hardware and microcode.
HOL4, HOL Light: hardware and floating-point proofs.
Isabelle/HOL: seL4-scale systems proofs, strong automation.
Rocq: verified compilers (CompCert), crypto (Fiat), big math proofs. Slow and hard to learn.
PVS: aerospace, much of NASA's formal methods work.
Agda: type theory research and teaching.
Lean 4: math (mathlib) and AI theorem proving. Hardest of the big three for LLMs off the shelf (27%).
Mizar, Metamath: large formal math libraries with simple checkers.
Verifying real code
SPARK: avionics, defense, rail.
Dafny: verified business logic, compiles to C#, Java, Go, Python, JS. AWS uses it for its authorization engine. Easiest for LLMs off the shelf (82%).
F*: verified crypto (HACL*, in Firefox and the Linux kernel).
Frama-C, Why3: C in safety-critical settings.
KeY, JML: Java.
VeriFast, Viper: separation-logic proofs about heap-heavy code.
Liquid Haskell: proofs added to existing Haskell.
Idris: general-purpose programming with dependent types.
Verus, Prusti, Creusot, Aeneas: proofs about Rust code.
WHY IT NEVER SCALED
Formal methods worked. They didn't scale, because a person had to write every proof.
Back to seL4. Its 8,700 lines of C needed roughly 200,000 lines of Isabelle proof, more than 20 lines of proof per line of code. IronFleet's verified distributed systems took 3.7 person-years, including inventing the method.
So formal methods stayed where a bug costs more than the proof: flight control, railways, crypto, kernels, cloud authorization.
Agents change that math. The proof is the tedious part, and an agent will grind on it all night. You also don't have to trust the agent, because the verifier accepts the proof or rejects it. What stays human is the spec. A green proof of the wrong spec is still wrong, so that's where your review time goes.
WHERE I'D START
I would start with the Verus formal language. The agent is the new part, so I'd pair it with a verifier that isn't. For agents writing verified code. It checks ordinary Rust against specs and proofs written in Rust, then erases them before compiling, so what you prove is what ships. It has peer-reviewed results since 2023, real systems built on it (Kubernetes controllers, OS kernel, etc), and use at Microsoft and Amazon.
For other jobs:
- Checking a distributed design: TLA+
- Math: Lean
- Bend 2, Vera, Vow and Kōdo: worth watching, still very early though.
Follow me for more on verification and agentic engineering.
Cristiano Calcagno retweeted
Don't learn formal methods.
Writing proofs by hand is what kept formal methods niche for over 75 years. seL4 took about 20 person-years to prove 8,700 lines of C. Agents take that part now. What's left for you is the spec, and knowing which language fits the job.
That's why the history matters. Formal methods means stating what a program or system must do in precise math, then using a tool to check that the code or design meets it. Here's how we got here, what each language is good for, and where I'd start.
FOUNDATIONS (1947 to 1979)
1947: Goldstine and von Neumann annotate program flow diagrams with "assertion boxes" stating what holds at each point.
1949: Alan Turing's "Checking a Large Routine" proves a short program correct using assertions. The idea mostly sits unused for over a decade.
1962: Carl Adam Petri's dissertation introduces Petri nets for modeling concurrent systems.
1963: John McCarthy, "A Basis for a Mathematical Theory of Computation".
1966-67: Peter Naur and Robert Floyd independently show how to prove programs with assertions attached to points in the code.
1967: N. G. de Bruijn starts Automath, the first language for computer-checked mathematical proofs.
1969: Tony Hoare publishes Hoare logic, {P} C {Q}. Nearly every contract language since builds on it.
1972: Robin Milner's Stanford LCF. Its Edinburgh successor (1979) introduces ML as its scripting language, the ancestor of Standard ML, OCaml and F#.
1973: Mizar starts in Poland. Formalized math that reads close to a textbook.
1975: Dijkstra's guarded commands and weakest preconditions.
1977: Amir Pnueli brings temporal logic to programs. Patrick and Radhia Cousot publish abstract interpretation, the theory behind sound static analyzers.
1978: Hoare's CSP for concurrent processes. Milner's CCS (1980) and the pi-calculus (1992) follow.
1970s: VDM at IBM's Vienna lab. Jean-Raymond Abrial proposes Z, later developed at Oxford. Boyer and Moore build their theorem prover.
TOOLS PEOPLE USED (1980 to 1999)
1981-82: Model checking, invented independently by Clarke and Emerson and by Queille and Sifakis. Turing Award in 2007.
1980s: Synchronous languages Esterel and Lustre in France. Lustre becomes SCADE, which Airbus uses to design flight control software.
1984: Nuprl at Cornell.
1985: Coquand and Huet's Calculus of Constructions, the logic under Coq.
1986: Isabelle (Larry Paulson).
Late 1980s: SPARK, a provable subset of Ada.
1988: HOL (Mike Gordon).
1989: Coq's first public release. Renamed Rocq in 2025.
1990: Symbolic model checking with BDDs handles 10^20 states. McMillan's SMV follows.
1991: SPIN model checker goes public (Gerard Holzmann, Bell Labs).
1992: PVS at SRI. Oxford and IBM win the Queen's Award for using Z on IBM's CICS transaction system.
1993: Metamath, a proof language simple enough to check with a few hundred lines of code.
1994: Lamport's TLA. TLA+ follows in 1999.
1994-95: Intel's Pentium division bug costs it $475 million. AMD uses ACL2, Kaufmann and Moore's successor to the Boyer-Moore prover, to prove its K5 floating-point division correct. Intel hires John Harrison in 1998 and uses his HOL Light to verify floating-point algorithms.
1996: Abrial's B-Book.
1997: Alloy (Daniel Jackson, MIT).
1998: Paris Metro line 14 opens driverless, with safety software built in the B method. The KeY project for Java verification starts.
1999: Agda (Catarina Coquand). JML, a contract language for Java.
VERIFIERS MEET REAL CODE (2000 to 2019)
2000: Microsoft's SLAM project starts. It ships as the Static Driver Verifier in the Windows driver kit.
2001-02: Separation logic (Reynolds, O'Hearn, Yang) makes pointer-heavy code provable.
2002: ESC/Java. Spec# (2004) and the Boogie verifier (2005) follow at Microsoft Research.
2003: Astrée proves the Airbus A340's primary flight control software free of run-time errors.
2004: CBMC, bounded model checking for C.
2005: Georges Gonthier finishes a Coq proof of the four color theorem.
2006: CompCert, a C compiler proved correct in Coq (Xavier Leroy). Event-B gets its Rodin toolset around the same time.
2007: Agda 2. Idris first appears (Edwin Brady).
2008: Z3 SMT solver (Microsoft Research). Frama-C. VeriFast.
2009: Dafny (Rustan Leino). seL4, the first general-purpose OS kernel with a machine-checked proof that its C code matches its spec.
2010: Why3.
2011: F*.
2012: A Coq proof of the Feit-Thompson odd order theorem is completed.
2013: Lean (Leonardo de Moura, Microsoft Research). P language at Microsoft.
2014: CakeML, a verified ML compiler. Liquid Haskell. Flyspeck finishes a formal proof of the Kepler conjecture.
2014-15: AWS reports TLA+ found bugs in S3 and DynamoDB that testing missed. IronFleet proves distributed systems correct in Dafny.
2015: Iris, a separation logic framework in Coq. Facebook open-sources Infer.
2016: Project Everest starts, aiming for a verified HTTPS stack. Viper.
2017: HACL*, verified crypto written in F*, ships in Firefox 57. Lean's mathlib starts.
2018: AWS Zelkova checks IAM and S3 policies with SMT solvers.
2019: Fiat Cryptography's Coq-generated code lands in BoringSSL, used by Chrome. Prusti for Rust.
LLMS MEET PROOF CHECKERS (2020 to 2025)
2020: OpenAI's GPT-f finds shorter Metamath proofs that get accepted into the main library, a first for deep learning.
2021: Lean 4.
2022: Kani (AWS) and Creusot for Rust. Aeneas translates Rust into Lean. The Liquid Tensor Experiment finishes the Lean proof Peter Scholze asked for.
2023: Verus for Rust. AWS releases Cedar, a policy language built with proofs in Dafny and later Lean. LeanDojo gives models a programmatic interface to Lean. Terence Tao's team formalizes the PFR conjecture proof in Lean in three weeks.
July 2024: DeepMind's AlphaProof reaches IMO silver-medal standard with proofs in Lean.
Sept 2024: Quint 1.0, TLA+ ideas with ordinary programming syntax.
Mar 2025: Imandra launches CodeLogician, an agent that turns code into its IML logic and checks it.
Apr 2025: AWS publishes how it rewrote its authorization engine, called a billion times per second, in Dafny with proofs.
July 2025: Harmonic's Aristotle reaches IMO gold-medal level with formal Lean proofs.
Sept 2025: The vericoding benchmark tests LLMs writing verified code from 12,504 specs. Off-the-shelf models pass 82% in Dafny, 44% in Verus, 27% in Lean.
LANGUAGES BUILT FOR AGENTS (2026)
Feb 22, 2026: Vera. "A programming language designed for LLMs to write, not humans."
Feb 25, 2026: Vow. "A Programming Language for Agentic Coding."
Mar 9, 2026: Kōdo. "Designed for AI agents to write." Z3-checked contracts, JSON errors with patches.
Sept 17, 2026: Bend 2. Dependent types and Lean-style proofs, C-like speed, CPU and GPU parallelism, Python-like syntax.
WHAT EACH LANGUAGE IS GOOD FOR
Specs and models
Z: precise requirements docs. Little tooling today.
VDM, B, Event-B: refining a spec step by step into code. Railways and safety-critical control.
CSP (with the FDR checker): concurrent protocols.
Petri nets: workflows and concurrent processes.
TLA+ and Quint: distributed system designs, consensus, race conditions before you write code. Checks the design, not the code.
Alloy: fast counterexamples in data models and access rules. Bounded, so finding no counterexample isn't a proof.
P: modeling and testing event-driven distributed services at AWS and Microsoft.
Model checkers
SPIN: concurrency protocols, as abstract models.
NuSMV and other SMV descendants: hardware and finite-state control logic.
CBMC: bounded checking of C code.
Kani: bounded checking of Rust, including unsafe code.
Static analysis
Astrée: proving embedded C has no run-time errors. Avionics.
Static Driver Verifier: Windows drivers using kernel APIs correctly.
Infer: memory and null bugs across large codebases.
Proof assistants
ACL2: hardware and microcode.
HOL4, HOL Light: hardware and floating-point proofs.
Isabelle/HOL: seL4-scale systems proofs, strong automation.
Rocq: verified compilers (CompCert), crypto (Fiat), big math proofs. Slow and hard to learn.
PVS: aerospace, much of NASA's formal methods work.
Agda: type theory research and teaching.
Lean 4: math (mathlib) and AI theorem proving. Hardest of the big three for LLMs off the shelf (27%).
Mizar, Metamath: large formal math libraries with simple checkers.
Verifying real code
SPARK: avionics, defense, rail.
Dafny: verified business logic, compiles to C#, Java, Go, Python, JS. AWS uses it for its authorization engine. Easiest for LLMs off the shelf (82%).
F*: verified crypto (HACL*, in Firefox and the Linux kernel).
Frama-C, Why3: C in safety-critical settings.
KeY, JML: Java.
VeriFast, Viper: separation-logic proofs about heap-heavy code.
Liquid Haskell: proofs added to existing Haskell.
Idris: general-purpose programming with dependent types.
Verus, Prusti, Creusot, Aeneas: proofs about Rust code.
WHY IT NEVER SCALED
Formal methods worked. They didn't scale, because a person had to write every proof.
Back to seL4. Its 8,700 lines of C needed roughly 200,000 lines of Isabelle proof, more than 20 lines of proof per line of code. IronFleet's verified distributed systems took 3.7 person-years, including inventing the method.
So formal methods stayed where a bug costs more than the proof: flight control, railways, crypto, kernels, cloud authorization.
Agents change that math. The proof is the tedious part, and an agent will grind on it all night. You also don't have to trust the agent, because the verifier accepts the proof or rejects it. What stays human is the spec. A green proof of the wrong spec is still wrong, so that's where your review time goes.
WHERE I'D START
I would start with the Verus formal language. The agent is the new part, so I'd pair it with a verifier that isn't. For agents writing verified code. It checks ordinary Rust against specs and proofs written in Rust, then erases them before compiling, so what you prove is what ships. It has peer-reviewed results since 2023, real systems built on it (Kubernetes controllers, OS kernel, etc), and use at Microsoft and Amazon.
For other jobs:
- Checking a distributed design: TLA+
- Math: Lean
- Bend 2, Vera, Vow and Kōdo: worth watching, still very early though.
Follow me for more on verification and agentic engineering.
Before AI I’ve dodged formal verification, benefited from static analysis (@fbinfer) and had lots of personal satisfaction from language design (@rescriptlang ).
Cristiano Calcagno retweeted
Are you interested in verifying UI layouts?
nitter.cf/gkurttech/status/21136…
@_chenglou's Handwired compiles programs into plain neural networks. That gave me an idea. If a UI is a neural network, the techniques used to verify neural networks can check it.
I first built a checker for Handwired itself to test the idea. Once that worked, I translated React Native’s layout engine (Yoga) into the same kind of circuit, and wrote checks like: does any element overflow its parent or overlap its neighbour, at any screen size and any text length?
It finds layout bugs a tester would likely miss, including a quirk in Yoga itself. Tests try a few sizes. But the checker covers every size and text length in a range. That means when a layout passes, it’s a proof of correctness, not just a sample. I’m very excited about what this opens up for UI testing.
Cristiano Calcagno retweeted
Isn’t that what we have @hillelogram and @VictorTaelin for? :)
Cristiano Calcagno retweeted
这条不喷A➗单纯聊一下技术。
感觉在AI时代Fuzzing和Formal Verification的地位可能要颠倒了。之前Fuzzing之所以更被青睐是因为大量的代码库难以被审计，所以才用动态执行的方法在不理解原程序语义的情况下“暴力”试出bug；而Formal Verification则因为需要比审计还要更大的工作量，所以完全impractical。但这个前提在能自动化理解大量代码的AI时代正在被慢慢瓦解，因为AI可以不断的尝试形式化验证不断的迭代试错，并在发现一部分代码不可能被验证的时候尝试找到导致其发生的漏洞。而这大概率比直接让AI审计找bug会更有效果，因为导致其不能被验证的原因可以作为找bug的hint，而这信息本质来源于作为外部的checker的形式化验证工具。随着针对形式化验证能力的RL和更好的验证方法，其能力应该还会提升。而当Linux或者Chromium这种级别的项目能被验证的时候，传统Fuzzing的历史使命也会彻底完成，不知道这一天何时到来。（又或者因为哥德尔不完备定理永远不会到来？）这就好比当黎曼猜想能被数学证明时，用计算机暴力求解非平凡零点的位置也将变得无意义。我作为一个曾经的Formal Verification黑，也不得不承认这一趋势。虽然我现在还在做Fuzzing相关的工作，但也在开始研究Formal Verification了。
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…
