AI makes formal verification central to software engineering
As code generation accelerates, Lean, Aristotle, and binary verification tools emerge to mathematically prove software correctness.
What to know
- AI code generation has become easy but unverified; traditional testing and code review are insufficient at scale, making formal verification urgent.
- Machine-checked proofs (via Lean, Aristotle, and binary verification tools) mathematically prove software correctness across all inputs, replacing probabilistic bug-finding with certainty.
- Harmonic raised $120M (Series C, $1.45B valuation) to bring formal verification to mainstream engineering; Zellic and V12 achieved end-to-end x86 binary verification.
- The field is shifting from trusting human review to trusting small, verifiable kernels—reducing the 'trusted base' and enabling AI-assisted security at scale.
Leo de Moura Lean creator, VP at AWSTudor Achim Harmonic CEO and co-founderHarmonic Formal verification software companyZellic and V12 Security and verification research firms
How it unfolded 3 developments, newest first · click a bar or a number to jump posts
-
3
Zellic and V12 achieve end-to-end x86 binary formal verification
Zellic and V12 published the first machine-checked proof covering the behavior of a Linux process executing a statically linked 64-bit x86 glibc binary end-to-end. Targeting the binary level reduces the trusted base compared to source-level verification and covers binaries from multiple compilers and languages, directly addressing security needs in AI-accelerated development.
“Formal verification is the big unlock that allows us to minimize the trusted base requiring security analysis.”
— Zellic and V12, Research collaboration · source -
I think the royal combo is Lean 4/TLA+/etc. plus AI plus a deterministic generator. For large systems formal method assertions need to be compressed down to a human comprehensible size. This can happen when the assertions are confirming the accuracy of a model and its attached code generators. The generator can generate proofs of the generated…
2 more of the top 3 · 12 posts in this stretch
-
Examples of comparing the results of Lean and e.g. Rust as is described in the video?I have symbolic error terms in Lean that I guess can be sampled and compared to Monte Carlo analysis? But I already had sampling-based analysis, that's why I had to do all of this (double-slit experiment and gravity with GrC(2,4)) in Lean 4.What would it take to…
-
"When AI Writes the Code, Who Proves It Works?" <- AI itself? Lol. Of course, not.Using AI to check AI is unavoidable. What us humans ought to do is *never* to give too much autonomy to AI. When we do so, we give up true intelligence that our work, lives and mankind depend on. Even when we mess up big time, as people, we are accountable for the…
-
-
2
Leo de Moura argues AI makes formal verification essential
In a podcast with Ben Lorica, Leo de Moura, creator of Lean and VP at AWS, discussed how AI's ease of code generation has made verification the critical challenge. He explained that Lean's machine-checked proofs address the trust bottleneck between humans and AI, moving beyond testing frameworks to mathematically prove code has no bugs.
“The proof is not informal. The proof is written in the Lean language, and more importantly, it's machine-checked.”
— Leo de Moura - 1 day quiet
-
1
Harmonic launches Aristotle formal verification for C and Verilog
Harmonic released Aristotle, extending its formal verification technology from research mathematics to software and hardware verification. The tool can mathematically prove whether specified properties hold across all possible inputs, addressing the verification bottleneck created by AI-generated code. Harmonic raised $120 million in Series C funding (valued at $1.45 billion) to support development.
“For businesses that rely on software and hardware, mathematically verifying critical systems provides a new way to identify defects and vulnerabilities before they become costly or catastrophic problems.”
— Tudor Achim
What people are saying 9 voices from 1 site · best of 12 · verbatim
- Nov 2
-
Addendum to my comment here - https://news.ycombinator.com/item?id=50317578I think i now have a decent top-level view of your architecture (courtesy some simple back-and-forth with Gemini in "AI Mode") and it is pretty good.Thanks for sharing.
- Oct 31
-
I guess I'm missing something but I don't see how this isn't just:1. Creating more work 2. Shifting the existing work to specificationThere's not really such a thing as a perfect specification. One of the things AI is taking away is character by character feedback cycles. Can't count how many times I'll be writing software and think in the middle…
-
I just don’t know why we are using a verification that is hard to read and write for humans
-
Isn’t the point of TLA+ is to model aspects of design at such high level that no deterministic generation is practical as a rule. The TLA+ models may be useful for LLMs (help find real bugs).
-
If you use agents to generate formal verification, how do you tell if the properties that are verified are the correct ones?
-
Very Interesting!Do you have a detailed paper/article written on this?> I think the royal combo is Lean 4/TLA+/etc. plus AI plus a deterministic generator. For large systems formal method assertions need to be compressed down to a human comprehensible size. This can happen when the assertions are confirming the accuracy of a model and its attached…
-
Currently the foundation theories in mathlib are built with the assumption that formal proofs are expensive. Concepts are fragmented to share as much proof as possible. With LLM the assumption is no longer correct. Concepts and proofs should be built to fit human thinking as much as possible and proofs can be ported by LLMs between theories. Lean…
-
What do people think of property based testing? I’ve set up a few property based tests and it feels almost like formal verification.I know it’s not the same thing, but PBT’s can catch all sorts of absolutely crazy bugs that I never would think to check for. Stateful stuff, cross-service stuff. My only gripe with PBTs has always been the tedious…
-
> ... But we expect, in the next few months and years, people will focus way more on the specifications, on the models, on the properties you want the software to have.Does anyone have resources on learning modelling for formal verification? (Does not have to be in Lean)