Vericoding: Formal Verification for AI Code Generation

Introduction

A programmer’s job is to translate human language, which is imprecise, into code, which is precise. Recent AI progress has popularized “vibe coding”, generating programs from natural-language descriptions, and with it an unprecedented volume of code whose quality is hard to trust. Today that code is guarded mainly by testing and human review before it ships into a world full of edge cases nobody anticipated.

Formal verification offers a stronger guarantee: a machine-checkable proof that code meets its specification, whether that spec is written by a human or, increasingly, generated by an agent. Despite a history reaching back to Turing (1949), it has remained niche, applied to a tiny fraction of software, because writing specifications and proofs by hand demands far more effort than writing the program itself. Verification and specification, not implementation, have always been the bottleneck, good engineers usually know what they want to build; they simply cannot afford to prove it correct.

That is what makes the present moment interesting. Generative AI can now help carry the burden, i.e. verifying existing code, or synthesizing new, formally verifiable code directly from a specification, a practice that has come to be called vericoding. Acting as an accelerant rather than a wholly new paradigm, AI promises to move formal verification from a niche discipline toward mainstream software engineering.

This article begins with a short background on formal methods and formal verification, then turns to formal verification in programming, and closes with a market map of the companies building in the field.

Formal Methods

What are formal methods?

Formal methods are rigorous mathematical and algorithmic techniques for the specification, design, verification, and maintenance of computational systems. At their core, they are about proof: you state proof obligations, prove that a system meets them, and synthesize a system that is correct by construction.

They are usually framed around three questions:

• Specification — what must the system do?
• Verification — why does it do that, or fail to?
• Synthesis — how does it do it?

To make the abstraction concrete, let’s look at a few examples depending on who is asking. A consumer buying a car asks whether it has the features they want. An engineer asks whether the implemented system meets its specification. A mathematician asks whether a mathematical model of the system satisfies a mathematical specification. Informally, all three are asking the same thing: does the system do what it is supposed to do?

Illustrative examples of formal verification (source: based on Sanjit Seshia’s lecture notes)

The toolbox for answering that question typically includes boolean satisfiability (SAT) and satisfiability-modulo-theories (SMT) solvers, model checkers, theorem provers, and simulation-based falsification.

Formal Verification

Formal verification is about automatically verifying the correctness of systems, i.e. confirming that a system does what it is supposed to do.

Why it matters

When a system fails to meet its obligations, the consequences can be severe. A few canonical examples:

• On June 4, 1996, the maiden flight of the European Space Agency’s Ariane 5 rocket ended 37 seconds after liftoff, when a software bug sent it off course and triggered self-destruction.
• The Intel Pentium FDIV bug, discovered in 1994 in the floating-point unit of early Pentium processors, caused certain high-precision divisions to return incorrect results — a controversy that ended in a roughly $475 million recall.
• Toyota recalled about 1.9 million third-generation Prius hybrids (2009–2014) over a software flaw in the hybrid system’s boost converter.

The same questions arise across distributed systems and everyday programming: does the program execute as intended? Does my secret data stay secret? Is the right program even being run? These concerns span cloud services, agentic AI, fintech, and ordinary application code. As AI works its way into cyber-physical systems, the case for formal verification only grows.

How verification is done

In practice, verification leans on the tools introduced above. SAT solvers handle tasks like equivalence checking of circuits and malware detection. SMT solvers extend SAT to richer types than Booleans and show up almost everywhere SAT does, i.e. software model checking, test generation, program synthesis, security-vulnerability discovery, and high-level hardware verification. Model checking, in turn, is a family of algorithmic methods that explore a system’s state space to decide whether it satisfies a formal specification.

A short history

• 1949 — the first program proof. Alan Turing sketches one of the earliest arguments that a program does what it claims.
• 1967 & 1969 — the mathematical foundation. Before anyone could build tools to check programs, the field needed a vocabulary for describing what a program actually does. Floyd’s work on program assertions and Hoare’s logic supplied the foundational rules for proving a program correct.
• 1977 — temporal logic. Ordinary logic handles static truths, but programs run dynamically. Pnueli introduced a way to specify properties over time, a breakthrough that earned him the 1996 Turing Award.
• 1981 — the birth of model checking. Clarke & Emerson, and Queille & Sifakis, shifted the field from manual proof to automated, algorithmic checking: represent a system as a state graph, and a computer can verify whether a property holds. The work earned them the 2007 Turing Award.
• 1999 — the industrial leap. When Clarke’s team introduced “Bounded Model Checking” using SAT, this was the tipping point that carried formal verification out of academia and into the standard industrial flow at companies like IBM, Intel, and Microsoft.
• 2005–present — the industrial adoption. Model checking and theorem proving matures for software and high-level hardware and it becomes part of the standard industrial flow.

Formal Verification in Programming

The number of bugs in software has fallen over the decades, at least until the widespread adoption of vibe coding. This decline is not due to any single breakthrough. A long list of technologies contributed: type systems, memory-safe languages, better software architecture (sandboxing, permissions, and the discipline of separating the “trusted computing base” from everything else), improved testing methodologies, a growing shared understanding of which coding patterns are safe and which are not, and ever-larger collections of pre-written, audited libraries.

One step short of formal verification sits property-based testing (PBT), already used to battle-test production systems across many enterprises. Instead of checking hand-picked cases, you state a property that should hold for every input and let the tool hunt for counterexamples. PBT can even run at the natural-language stage: the user clarifies intent, an LLM turns it into candidate properties, and the specification is hardened from the outside. Thus it can help non-expert users define what the spec should be in the first place. The catch is depth, i.e. PBT tests a property on sampled inputs, while formal verification proves it for all of them.

Formal verification with AI assistance is not best understood as a brand-new paradigm, but as a strong accelerant for one that was already advancing. What AI adds is efficiency and ease.

Spec, Code, and Proof

Every formal verification system has three components:

• Spec — a mathematical formalization of human intent: what a program is allowed to do, and what it must never do.
• Code — a set of executable instructions.
• Proof — a mathematical argument that the Code satisfies the Spec.

Historically, the Spec and much of the Proof had to be written by hand, expensive enough that it only made sense in select domains such as core cloud infrastructure. Generative AI promises to change that by automating parts or all of the pipeline.

The common approaches to “AI for formal verification” sit on a spectrum:

• Provers — humans write the Spec and Code, and AI invents the Proof.
• Vericoding — humans provide a careful formal Spec, carrying much of the semantic burden, and AI synthesizes the Code and Proof.
• End-to-end vericoding — humans describe a system in natural language, and AI produces the Spec, Code, and Proof from scratch.

Vericoding is the LLM generation of formally verified code from a formal specification, i.e. the disciplined counterpart to vibe coding, which produces potentially buggy code from a natural-language description. A program counts as formally verified when the formal verification system’s checker confirms that the Proof demonstrates that the Code satisfies the Spec. The guarantee is unusually strong, but also narrower than it first appears: it shows that code adheres to a formal specification, not necessarily to the original human intent behind it.

Or as Donald Knuth might say:

Beware of bugs in the above code; I have only proved it correct, not tried it.

That caveat reframes the discipline. As AI takes over implementation, specification, i.e. precise descriptions of what software must do, becomes the central engineering skill. Writing a spec forces clear thinking about what a system must do, which invariants it must hold, and what may go wrong. It is not hard to imagine a future in which humans write specs rather than programs.

Formal programming languages

Systems that produce and certify mathematical proofs can be divided into interactive theorem provers (ITPs), which check user-supplied proofs, and automated theorem provers (ATPs), which attempt to prove theorems autonomously (and often fail). A recurring prediction is that future AI-generated software will be verified by autonomous verification agents steering ITPs, much as coding agents steer software production today. Historically, the bottleneck has been the small number of human experts able to write ITP proofs at all.

The programming language Lean is emerging as the de facto standard at the proving-heavy end of the field. AlphaProof (Google DeepMind), Aristotle (Harmonic), Seed-Prover (ByteDance), Axiom, Aleph (Logical Intelligence), and Mistral AI’s Leanstral all build on it. Like **Rocq/Coq**, Lean is an interactive theorem prover: you state a theorem and construct a machine-checked proof of it, built on dependent type theory in which the proof is an explicit term verified by a small, trusted kernel.

**Dafny and [Verus](https://verus-lang.github.io/verus/guide/)** take a different route, as auto-active verifiers: you write code alongside specifications, and the tool compiles the correctness conditions into queries for an SMT solver (the automated prover under the hood) which tries to discharge them with no further human input. When it works, you get verified code without writing a proof by hand. This trade-off is the heart of the matter: Dafny and Verus are often faster for everyday program verification, while Lean offers more expressive power and finer control for properties an SMT solver cannot settle on its own, checking an explicit proof term against its small kernel and thereby shrinking what you must trust rather than delegating it to a solver.

Checking at machine speed

A guarantee is only as valuable as it is cheap to check. Formal verification has always rested on an asymmetry, i.e. a proof may be expensive to produce but should be far cheaper to verify. Yet that asymmetry collapses at scale: if a proof takes ten minutes to produce and another ten to check, it is of little use. Adding cryptography (ZK proofs) to the loop restores it. Succinct cryptographic proofs can verify the whole chain from natural language → spec → formally verified code in less than a second. That is what lets vericoding keep pace with vibe coding.

The other direction: formal methods for trustworthy AI

The relationship runs both ways. Just as AI can foster formal verification, formal verification can make AI more trustworthy by giving stronger assurances, often labeled “trustworthy AI” or “AI safety.”

Many critical functions are now implemented by AI components generated from data rather than programmed by hand, and these components increasingly drive autonomous cyber-physical systems in self-driving cars, smart grids, healthcare, and manufacturing. Deep neural networks, for instance, are now essential to perception and object classification in autonomous vehicles.

Yet data-driven behavior is inherently hard to characterize, and combining it with traditional, rule-based engineering tools is not well understood and can introduce new risks. Recent Trustworthy-AI initiatives call for designing and operating such systems so that they meet safety, security, privacy, robustness, legal, ethical, and explainability requirements appropriate to the application: AI provides the autonomy, and formal, model-based techniques provide the guarantees.

Cyber-physical systems where AI provides the autonomy

This article focuses on formal verification in programming rather than for trustworthy AI. The latter is a rich topic in its own right, and arguably deserves an article of its own.

Projects Working on Formal Verification for AI Code Generation

The map is organized along the Spec → Code → Proof pipeline.

AI provers

Companies building the AI that writes the proof itself, given a goal already stated in formal logic. These are the engines much of the rest of the map depends on: AlphaProof (Google DeepMind), Aristotle (Harmonic), Seed-Prover (ByteDance), Axiom, Mistral AI’s Leanstral, Math Inc., DeepSeek-Prover, and Aleph (Logical Intelligence), whose energy-based approach stands somewhat apart.

End-to-end vericoding: natural language into formal spec, code and proof

AI that turn ambiguous human intent into a precise formal specification, code, and proof. ICME’s PreFlight converts natural-language policies into formal logic checked by an SMT solver and wrapped in a cryptographic proof. Galois envisions a workflow in which a designer refines a specification with an AI assistant through natural language, moving from an incomplete state to one that supports formal verification. Bloom is built on the premise that specs are public, with other humans and agents incentivized to find gaps and propose better invariants. Astrogator proposes a knowledge base to capture system-specific dependencies and reduce the system knowledge needed to express formal queries.

Vericoding: AI generates verified code from a spec

Companies where you supply the formal spec and the AI synthesizes both the implementation and its proof, such as Code Metal, Cocotec or Scidonia which combines LLMs with symbolic reasoning and formal constraints for high-stakes domains where mistakes are irreversible.

Provers: verifying existing code

Companies that prove properties about code that already exists rather than generating anything new. This is the established formal-methods industry now adding AI: AdaCore, TrustInSoft, Runtime Verification, Formal Land, or Imandra.

Ecosystem, research, and nonprofits

Organizations that build the shared infrastructure, benchmarks, and open proofs the commercial layers draw on, rather than selling a product, such as Apart Research, Beneficial AI Foundation, or Forall R&D.

Source: view this market map as a table

As with any young and fast-moving field, this map is far from comprehensive, and it is likely to look quite different in just a few months. Also, the categories overlap at the edges.

If you think a project is missing or miscategorized, please DM.

Closing Words

As LLMs produce ever-larger volumes of code of uncertain quality, the case for moving from vibe coding to vericoding becomes hard to ignore. The engineer’s role changes, but it does not shrink. More time goes into writing specifications and models, designing systems at a higher level of abstraction, and stating precisely what a system must do, which invariants it must preserve, and which failures it must tolerate. The work becomes more creative, not less. Productivity comes not from generating more code, but from generating code that is provably correct on the first attempt.

If the cost of verification falls toward zero, every domain where correctness matters speeds up. Aerospace, automotive, and medical-device certification, which today take years of qualification effort, could collapse to weeks; cloud providers face similar effort qualifying security-critical services and cryptographic implementations; and hardware verification, where a single bug can cost hundreds of millions of dollars, benefits just as much.

Each verified component is also a permanent public good. Unlike proprietary software, a verified open-source library cannot be quietly degraded, have its guarantees revoked, or be held hostage to one company’s business decisions. The proofs are public: anyone can audit them, build on them, or swap the implementation while preserving the guarantees. This is infrastructure in the deepest sense.

Acknowledgements: this article draws on prior writing, including Vitalik Buterin, ICME, Leonardo de Moura, Logical Intelligence, zkSecurity, Sanjit Seshia’s Berkeley lecture notes, the Shonan report on formal methods, and publications by Bursuc et al., Blain & Noiseux, Councilman et al., and Dougherty et al.

If you are building something in vericoding or formal verification, or using it in production, please reach out!

Many thanks to Valeriy Zamaraiev, Wyatt Benno and Gavin Pacini for conversations around this topic.

You could follow me on X and LinkedIn.