AI coding agents now write code faster than any team can read it line by line, and that gap is pushing formal verification, the practice of mathematically proving that software meets its requirements, out of its niche. One firm that specializes in the field found long-hidden bugs in the Linux kernel, and one of them surfaced before any proof was attempted: it appeared while the team was writing down what the code was supposed to do. The lesson the firm draws is that as AI takes over the “how” of software, the human job shifts toward stating the “what” precisely.
Prove it first instead of testing it later
Engineers who design a bridge do not drive cars across it to see whether it collapses. They calculate load, wind shear and stress tolerances in advance. Software took a different path because code was cheap and easy to change, so an iterate-and-test cycle became the norm. The firm’s CEO argues that software failures can now be as severe and as costly as a bridge collapse, which makes rigorous mathematical methods worth the effort.
The company’s founder, a computer science professor at the University of Illinois Urbana-Champaign (UIUC), frames the core idea in three parts:
- A specification defines what a system must accomplish.
- Code determines how it accomplishes it.
- Mathematics is the bridge that proves a given “how” satisfies the stated “what.”
Formal specification research dates back to the 1960s, yet no single specification language has ever won industry-wide agreement, much like programming languages themselves. Writing exhaustive specifications has also been slow and tedious. Recent AI models change that by turning natural-language intent into formal specifications much faster. The firm trains models to take a developer’s intent and produce the specification and the code together, and it expects a future in which AI delivers code, specification and proof as one bundle while humans mainly check the result.
What writing a spec revealed in the Linux kernel
In October 2026 the firm published a report on a Linux bug in which user identity mappings were silently handled incorrectly. The team found it while writing the specification. Its work concentrated on the boundary where the kernel accepts and parses untrusted input from user space. To define correct behavior, the team pulled together old forum posts, developer mailing list threads, documentation and source code, and turned them into formal rules. According to the firm, that step almost always exposes places where the code has quietly drifted from what its developers intended.
Why did open-source review miss the flaw despite the belief that enough eyes make every bug shallow? The firm’s hypothesis is that peripheral subsystems such as device drivers get far less scrutiny than high-profile core code like the scheduler, even though they handle untrusted input.
Rather than simply prompting a large language model (LLM), the team used a staged process:
- Engineers inspected the code and the formal requirements by hand.
- An LLM ported the legacy C code to Rust, a memory-safe language.
- The team ran differential fuzzing, which feeds the same random inputs to the original C version and the Rust port and flags any difference in behavior. This quickly surfaced divergences and logic bugs.
- Attempting formal proofs of the Rust version uncovered deeper edge-case flaws that fuzzing had missed.
▲ Differential fuzzing across two implementations
The work ran in strict two-week timeboxes. Targets included the USB Video Class (UVC) driver, which streams video data over USB, and the Android Binder IPC subsystem, and the team verified 80 or more theorems. The parts left unverified were not unprovable; each sprint simply ended on schedule so the team could move on and package its methods into reusable tools. The setup was modest: mostly a single Claude Code instance on a standard premium plan. The bottleneck was engineering time, not tokens or compute. Wherever possible, techniques an LLM discovers are turned into deterministic testing tools that give the same result every run.
Kernel maintainers are already worn down by a flood of low-quality AI-generated patches, and they have said plainly that they will not accept or maintain separate Lean or Rust code for kernel drivers. Lean is a language for writing mathematical proofs that a machine can check. So the firm keeps its Lean and Rust models in-house and sends maintainers only high-signal C patches. Its first pitch of formal verification as such was turned away; maintainers began to welcome the collaboration once the firm showed reproducible bugs and ready-to-merge fixes.
Verification habits any developer can adopt now
You do not need deep formal-methods expertise to add verification to AI-assisted coding. The firm’s advice breaks down by stage:
| Stage | What to do | Why it helps |
|---|---|---|
| Before generating code | Ask a model such as Claude Opus 5.5 for a detailed multi-step plan, keep it in the repository and review every line | Aligns your intent with the model’s plan; the reviewed plan becomes a pseudo-formal spec |
| When porting code | Have an LLM build a differential fuzzing harness that compares two implementations | Pinpoints porting errors and legacy bugs |
| After generating code | Ask an agent to write a Lean specification of the new code and prove it correct | Forcing the model to state exact invariants exposes hidden logic flaws |
| At third-party boundaries | Specify preconditions and postconditions for every API that touches unverified libraries | Gives you a basis for catching misuse between components |
The first habit comes with a military saying: slow is smooth, and smooth is fast. Do not let the model jump straight into code until its plan matches what you want. The founder calls the third habit “code review plus plus,” because most bugs show up not while proving theorems but while writing down, formally, what the program is meant to achieve.
When verification starts paying for itself
Formal verification has long been treated as doubling engineering effort. The firm’s own estimates look like this:
| Approach | Effort relative to building without verification |
|---|---|
| Traditional formal verification | About 2x |
| Verification built in early in development | About 1.1x to 1.2x |
| Early verification plus LLMs translating between formal models and runnable code | About 0.8x, a net saving |
The firm points to Amazon’s Cedar, an identity and access management policy engine re-architected in Rust from Java and Kotlin and formally verified, as an enterprise success: it runs three times faster while carrying formal security guarantees. The broader lesson, in the firm’s view, is that mandates will not spread verification. Tools have to slot into developers’ daily workflow and deliver value right away.
Agent safety: verify the monitor, not the model
Proving that a neural network’s weights are correct, or that a vast legacy operating system stack is correct, is practically impossible. The founder’s answer is the runtime monitor, a lightweight program that watches a running system. A monitor is small enough to verify formally. A verified monitor draws a safety envelope around an autonomous agent and either steers it back into safe bounds or triggers a fallback when it crosses the line. The agent’s reasoning may remain unverified, but catastrophic actions can still be blocked. The approach grows out of research the founder began at NASA in 2001.
The firm argues that this does not limit an agent’s creativity. Verified components work like Lego bricks stamped with a mathematical proof: whatever the agent builds on top, the base will not crack. Unverified AI-generated code, on the other hand, stays easy to exploit, and the firm warns that automated hacking could let a lone attacker break into complex infrastructure such as NASA’s when systems lack formal verification.
▲ A verified safety envelope around an AI agent
There are limits worth weighing. Reinforcement learning from human feedback, or RLHF, was conceived as a safety method but ended up as a major capability boost that sped up commercial deployment. Formal verification may follow the same path, giving agents reliable tools without guaranteeing their intentions. A verified sandbox and package manager can stop an agent from escaping, but they cannot ensure the model will not pursue the wrong goal. Stronger guardrails may also create a false sense of security that leads organizations to hand real-world authority to models that are still untrusted. Even if misalignment becomes rarer with each model generation, much longer autonomous task horizons could mean that routine work looks flawless while the rare failure is a large one.
The takeaway: state intent before you write code
The firm’s CEO predicts that hand-written code will be largely obsolete within two years, and that within two to five years package ecosystems such as npm and Cargo will increasingly require formal specifications and Lean proofs. He also expects, within 24 months, comprehensive formal models of the Linux kernel’s C code alongside Rust translations proven to behave identically, though upstream maintainers may not adopt them right away. These are one company’s forecasts, but the direction, with verification effort moving from writing code to defining intent, appears worth planning for now.
For developers and teams building software with AI:
- Get a design plan from the model before any code, keep it in the repository and review it line by line.
- When you port or rewrite an implementation, add differential fuzzing that compares the old and new versions on identical inputs.
- For critical modules, have an agent write a Lean specification and proof as a deeper form of code review.
- Write preconditions and postconditions for every API boundary that touches unverified third-party libraries.
- Before connecting an agent to real systems, put a monitor that enforces its allowed actions, plus a manual fallback, in place instead of relying on the model alone.