What Software Can We Verify Today?, Part 3

11 Case Study: Aristotle

Harmonic's Aristotle is the commercial system most often cited as proof that AI has reached software verification. Read its results as five connected modes of use, each with a different specification and a different thing left outside the proof.

Olympiad Mathematics

Start with the easiest case. Aristotle reached gold-medal-equivalent performance on the 2025 IMO problems. The specification is the problem statement, the checker is Lean's kernel, and the search space is closed. The rest of the post is about a harder case: the model translating a C program or guessing what a hardware block should do. Here it is proving a theorem someone else stated.

RTL Against an ISA Model

The first systems example is hardware. Harmonic pointed Aristotle at the multiply and divide instructions of the Ibex RISC-V core and compared the RTL against the Sail model of the ISA. It proved nine properties: assertions for MUL, MULH, MULHSU, MULHU, DIV, DIVU, REM, and REMU, plus a termination property that keeps the assertions from passing vacuously.

The run covered division by zero and the signed overflow case, with no environment assumptions, and it also proved MUL on the fast multi-cycle multiplier. The specification is external and formal (the Sail ISA), so the proof is a refinement check between two models, not a proof that Ibex as a whole is correct.

A Whole Block, Refuted and Proved

Hardware is where formal verification is already routine, and the economics explain why. A software bug ships with a patch; a bug in silicon ships in every chip, and fixing it means a new tape-out that costs months. So chip teams run commercial model checkers over their RTL, proving assertions about the design before it is manufactured. The limits are scale and people. The state space grows exponentially with the number of flip-flops, so formal tools are usually pointed at small blocks or asked to search a bounded number of cycles past reset, and the properties are written by hand by a scarce kind of engineer.

The scale jumps at Tensordyne, which builds AI inference systems. Jonathan Ko, an ASIC verification engineer there, picked the block he considered hardest to verify: 12.2 million gate equivalents, 1.24 million flops, 45 Mbit of SRAM, hundreds of concurrent state machines, and 312 pages of specifications. "Even sub-blocks a tenth this size are very difficult to formally verify with traditional tools," he says in Harmonic's case study. Aristotle wrote 100 properties from the specs and took 141 assertions already in the RTL, proved 185, and refuted 56 with reproducible counterexamples. According to Harmonic, every proof covers the whole block from power-on, for every input sequence the environment allows, with no bound on the number of cycles. The refutations exposed bugs 25,000 to 110,000 cycles after reset, past roughly 24,600 cycles of memory initialization; Tensordyne found eight bugs early in the design cycle.

That is why the result matters. Bugs that deep sit behind long setup sequences, where bounded searches rarely look and random simulation rarely drives the design, and the properties came from prose specifications rather than a verification engineer's hand. These are vendor-reported numbers I could not check independently. If they hold, the bottleneck in hardware verification moves from writing and running properties to deciding whether the specification and environment assumptions are right.

The same run also shows the limits of a proof: 56 refutations are counterexamples, and the 185 proofs are conditional on the specs, the wrapper, and the environment assumptions. In a second project, Aristotle wrote RTL from a spec, proved 37 properties, and after synthesis feedback produced an early block with about 26% less power.

C, Repaired and Optimized

The C case matters most here. On LibTomMath, Aristotle found and repaired three bugs: (1) a missing size check in fast squaring, which could write past a stack array on an oversized direct call; (2) the same missing check in Montgomery reduction; and (3) a comparison helper that could form a pointer before the start of an array when comparing equal numbers. It then proved the repaired routines and their helpers against specifications for results, memory safety, errors, and stored values, and optimized two arithmetic routines while preserving those specs. Modular exponentiation ran 31–38% faster in Harmonic's benchmarks.

A Walkthrough: The Comparison Bug

The comparison bug is small enough to show in simplified form. The helper compares the magnitudes of two numbers of the same length digit by digit, starting from the most significant digit and stopping at the first one that differs:

/* before: empty inputs can form a pointer before the array */
const mp_digit *pa = a->dp + a->used - 1;
const mp_digit *pb = b->dp + b->used - 1;
while (pa >= a->dp && *pa == *pb) { pa--; pb--; }

/* after: indexes cannot form a pointer before the array */
for (i = a->used; i-- > 0; ) {
    if (a->dp[i] != b->dp[i]) {
        return a->dp[i] > b->dp[i] ? MP_GT : MP_LT;
    }
}
return MP_EQ;

The trouble is the case where every digit matches. The old loop keeps stepping down until pa sits one element before the start of the digit array, and only then does the pa >= a->dp test stop it; for two numbers with no digits at all, the pointer starts there. Nothing is ever read through that pointer, which is why tests pass. But in C, merely computing a pointer before the start of an array is undefined behavior, and so is the comparison that relies on it. A compiler is entitled to assume pa >= a->dp always holds and drop the check, which would turn comparing two equal numbers into an out-of-bounds read. The fix counts an index down instead, so the loop ends at zero without ever forming the bad pointer.

Aristotle's project page records the pair directly: the pre-fix comparison is refuted, the fixed one proved, alongside 18 proved and 3 refuted properties in total.

18 PROVED · 3 REFUTED

MP_CMP_MAG.MEMORY_SAFETY_AS_SUBMITTED
  REFUTED
  Memory safety ... of mp_cmp_mag(a, b) as originally
  submitted (before the fix).

MP_CMP_MAG.MEMORY_SAFETY
  PROVED
  The call has no undefined behaviour: it only reads
  a->dp[i], b->dp[i] ... never forms an out-of-bounds
  pointer.

A Backend for Other Agents

The last mode puts Aristotle inside someone else's loop, as the closer for proofs another agent started. LeetProof, the pipeline from the Velvet discussion in Part 1, gives GPT-5.2 a $5 budget per problem to write the code, invariants, and proofs. When the budget runs out, some problems are left partial: the program and its specification are fixed, the verification-condition generator has split correctness into separate obligations, and most of them are discharged, but a few goals remain open. Handed those leftovers, Aristotle closed all 18 partially proved Velvet programs and 23 of the 30 single-mode partials.

A residual goal is easiest to picture on the sumUpTo program from route C. Showing that the loop body preserves the invariant leaves an obligation of this shape:

i n acc : Nat
h₁ : i < n
h₂ : 2 * acc = i * (i + 1)
⊢ 2 * (acc + (i + 1)) = (i + 1) * (i + 1 + 1)

Every hypothesis is in place and the statement is true, but the arithmetic is nonlinear, which is where linear decision procedures such as omega stop. A human closes it by expanding both sides and substituting h₂; a tactic search has to find the same step. Real residuals carry more hypotheses and longer terms, but they have this shape.

The work is proof repair on residual verification conditions: the goal is already stated, and the question is whether a tactic search can close it. Nothing about the program or the specification changes, which makes this the easiest of the five modes to trust. It also accounts for the gap in Figure 6 in Part 1: the Velvet residuals had already passed property-based testing, so they were almost certainly true, while the seven single-mode goals Aristotle could not close had passed no such filter.

Together, the examples show a consistent division of labor. Aristotle is strongest when the specification is already formal and the remaining job is search, repair, or refutation: an IMO statement, a Sail ISA, a set of RTL assertions, C contracts, or a Lean verification condition. The hard part stays where this post has put it: deciding what the artifact should do, and what the model of the machine is allowed to assume.

12 Case Study: Theorem and Anthropic

The other large public result takes the opposite approach to Eita. In October 2026, Anthropic's Frontier Red Team and Theorem reported that Claude proved crash-freedom for 239 entry points across 123 OSS-Fuzz libraries, on the compiled RISC-V binaries, for every input under 64 MB and every modeled OS response and memory layout. The specification was not written by hand: each OSS-Fuzz harness, built with AddressSanitizer, became the property "this harness never crashes," and Theorem's RISC-V and Linux-process semantics turned binary plus property into a Rocq theorem. The accepted proofs total about 180 million lines of Rocq, with typical proofs around 600,000 lines per entry point, out of about a billion lines Claude wrote, and the attempt surfaced hundreds of bugs.

The Three Theorems Behind a “Crash-Free” Claim

The headline is a stack of three claims, not one. The appendix spells them out for two binaries, an ASan-instrumented fuzz build and the normal build, on RISC-V Linux, for all inputs under 64 MiB and all memory layouts:

1. The ASan binary never faults, aborts, or hits unmodeled behavior.
2. The ASan binary and the normal binary produce the same read/write trace, exit the same way, and leave the file system in the same state.
3. The normal, uninstrumented binary never crashes either.

Only the first is what the fuzz harness directly tests. The second is what makes the first relevant to the binary users run, and the third closes the branch where the ASan build loops and the normal build crashes.

Most of that volume is not about the libraries at all. The appendix notes that in cJSON's roughly 630,000-line proof, only about a tenth concerns cJSON; the rest covers C start-up, the allocator, printf, the sanitizer runtime, and the fuzz driver. Figure 1 shows where the lines go.

A Fuzz Test Becomes a Theorem

The LZO fuzz target is the cleanest code example; this is the appendix's version, lightly simplified. It compresses its input, decompresses the result, and asserts that both calls succeed and round-trip the byte count:

r = lzo1x_1_compress(data, size, compressed, &compressed_len, wrkmem);
assert(r == LZO_E_OK);
if (compressed_len >= size) goto join;
decompressed_len = size + 1;
r = lzo1x_decompress(compressed, compressed_len, decompressed, &decompressed_len, NULL);
assert(r == LZO_E_OK && decompressed_len == size);

Those two assert calls are the specification. The proof steps through the branches at their exact RISC-V addresses and shows neither abort path is taken. Because the assertions encode round-tripping, the proof establishes LZO's compression/decompression round-trip, not just memory safety.

What the Proof Looks Like

A finished proof is not a short Rocq lemma. It runs to about 600,000 lines across 1,400 files; over half is machine-emitted instruction encodings and lookup tables, and about 40% is proof text. Checking one proof takes 30 minutes to several hours.

• Agent proofs are verbose. They spell out register contents, address distinctness, integer conversions, and every branch.
• Human proof engineers abstract. They would factor those details into calling conventions, disjoint-pointer predicates, and allocator abstractions.
• The abstraction is inconsistent. Agents introduced some of these constructs, but not consistently; the gap between a valid proof and a maintainable one is the scalability question the appendix raises.

The first surprise is that proof size barely tracks code size. cJSON's 391-line parser entry point got a 630,000-line proof; fftw3, with 51,000 lines linked in, got 480,000. The median specification was 110 lines against a median program of 86 KB, and the proofs cover roughly 20–50% of the code the fuzz driver exercises. A proof is a statement about a whole process, not a line-by-line annotation of the library.

The second is that proofs are reusable. Most of a binary proof concerns C start-up, the allocator, printf, and the ASan runtime, which every program shares. When agents could copy each other's proofs, they needed 17% fewer tokens, and some succeeded after failing alone. That is the Mathlib pattern applied to systems code: the unit of reuse is a lemma or a file, not a whole proof.

Not every proof in the report is a 600,000-line binary proof. The Python-interpreter experiment used Verus: 17 tiers, one theorem per tier, and the statement that "whenever the interpreter returns a result, that result is the one the formal semantics prescribes." The team injected seven bugs into an early version; five survived the random tests, and all seven broke the proof. That is the cleanest demonstration in the report of what a proof catches that testing does not.

The two projects bracket what we can verify today. Theorem's result is route E at scale: unmodified code, a generated specification, a trusted base of the ISA model, the OS model, the theorem statement, and the Rocq checker. Its property is shallow but universal. Eita's is a new implementation of a well-specified system with deep functional properties, partially proved, and a trusted base that includes the specification translation.

Both teams are explicit about the limits. Anthropic's post says that "formally verified" does not mean bug-free, and that its proofs cover single-threaded static RISC-V binaries linked against musl, while most users run these libraries on x86 or ARM against glibc.

The Same Route, a Deeper Property

Less than three weeks after the Anthropic report, Google DeepMind published AlphaProof Code, which takes route E toward a much richer property than crash-freedom. The target is libsignal, the reference implementation of the Signal protocol. The team wraps the unmodified Rust crates in a small command-line harness, compiles it with stock rustc into a static AArch64 Linux executable, and states its theorems in Lean over whole runs of that executable. What the agents proved is protocol-level security: forward secrecy, post-compromise security, authentication, and handshake secrecy for the post-quantum PQXDH handshake and the Triple Ratchet, in both the symbolic and the computational model of cryptography.

The paper's numbers are easy to set beside Theorem's. A team of five worked for four weeks and wrote no proof code; campaigns of 40 to 80 agents ran for one to three days each on a single machine. The result is about 6.5 million lines of Lean proof for roughly 140,000 AArch64 instructions, resting on about 18,000 lines of trusted specification and 8,000 lines of instruction-set semantics. As in the RISC-V proofs, most of the text is about the machine: 5.3 million of those lines establish what the binary does, and the two security arguments built on top take about 860,000 and 350,000.

What the five people did instead was write specifications, and the paper says so directly: "The majority of our effort went not into proofs but into specifications." Each draft was reviewed by an agent from a different model family, and the agents then had to show the specification was not vacuous: that its hypotheses are jointly satisfiable, that mutating the code (skipping the MAC check, say) makes the security theorem provably false, and that two previously fixed libsignal bugs, reintroduced into the binary, each yield a complete Lean proof that the theorem fails. Along the way the exercise turned up errors in the published analyses it started from, including fifteen gaps or bugs in the computational analysis of the Double Ratchet.

The prover agents cannot touch the specification. A gatekeeper holds a copy that no agent can write to, and accepts a proof only when the statement and every definition under it match that copy and Lean's kernel accepts the proof with no sorry. An agent that finds the specification wrong about the code can propose a small amendment to a critic that never sees the proof attempts, and anything that would weaken security goes to a human as a potential bug. This is the "Certifiably Wrong" failure from Part 1, handled by process.

The limits are stated as carefully as the result. About forty routines are replaced by trusted contracts at the binary boundary: the low-level cryptographic primitives, five libc memory routines, and the functions that write output. Key generation is not verified, only one-to-one sessions are covered, and the theorems concern DeepMind's harness build, not Signal's own apps. The computational bound holds against classical attackers only and becomes vacuous at scale, for a single session of about 25,000 messages if nearly every message starts a new epoch. The symbolic theorem excuses byte collisions without bounding their probability.

So the bracket above needs a third point. This is unmodified production code with a deep property, which neither Eita nor Theorem's result offers. It is also the case with the most favorable conditions for specification: a protocol whose security had already been formalized in the research literature, and five experts spending most of four weeks adapting those models to the code. Theorem's specifications were generated from fuzz harnesses; these were engineered by hand, with agents assisting. The proving was automated, and the specification is where the people's time went.

13 A Blueprint for a Verification Pipeline

Suppose you own a security-critical component, an authorization kernel, a cryptographic routine, an enclave boundary, a consensus state machine, and you want to use AI and Lean on it without landing in the Lean tarpit or certifying a vacuous specification. Here is what the evidence supports.

Isolate the Stateful Core

Do not try to push a 200,000-line application through route A. Use a functional-core, imperative-shell design and pick the route by what the core is. For new or refactorable code, write the decision kernel in safe Rust with no I/O and extract it with Aeneas (directly or through hax), pinning one Lean toolchain across Aeneas, Mathlib, and Batteries before the first proof. For algorithms, write them in Velvet where testing and VC generation run first. For legacy C, assembly, or RTL you cannot change, lift the source or the binary.

Falsify Before You Deduce

Never hand an unvalidated program or invariant straight to a heavy prover. Arrange the pipeline left to right, with each stage cheaper than the next and rejecting what it can. Figure 2 is that pipeline.

In the LeetProof study, nine minutes of property-based testing found 13 of the VERINA specification bugs, while checking specification equivalence with an AI prover took around eight hours. The same filtering applies inside tree search: run a counterexample finder on candidate subgoals before expanding them.

Ground Premise Selection

To get past the 60% wall, do not let the model guess lemma names from its weights. Expose the live goal through a fast REPL, pair the model with a symbolic relevance filter that injects the hundred or so most relevant local lemmas, and repair unknown identifiers by edit distance automatically.

Verify Bottom-Up

Composition is where today's models collapse, so do not ask them to compose. Walk the call graph from the leaves up, prove each callee against its contract, and freeze that contract before any caller's proof starts. When a caller's proof stalls, suspect the callee's postcondition first: check with a quick property test whether the fact the caller needs follows from the callee's contract at all, and if it does not, strengthen the contract and re-prove the callee instead of searching harder in the caller. Keep frame conditions small by keeping callees pure where you can, so each call does not drag every untouched field into the goal.

Keep the Inner Loop Local

Use small local models in the high-frequency loops, proposing invariants, repairing single steps, and discharging routine obligations alongside lean-smt and grind. Abstract the hard residue into self-contained algebraic or bit-vector lemmas with the business logic stripped out, and send only those to a frontier prover. That addresses confidentiality, reproducibility, and cost together.

Gate the Prover Mechanically

An agent rewarded for "Lean exits 0" will exploit every gap. That is measured: on ImpossibleBench, frontier coding agents special-cased or edited contradictory tests most of the time, and making the tests read-only was among the mitigations that worked. The CI harness has to close the gaps deterministically:

• Axiom gate. Run #print axioms on each theorem from a separate, read-only file and reject sorryAx, Lean.trustCompiler, and any axiom the agent introduced.
• Independent kernel. Export the environment and re-check it with a second kernel implementation such as nanoda, as the July 2026 kernel postmortem recommends; a forged proof can show a clean axiom list.
• No escape hatches. Reject partial def, unsafe def, @[implemented_by], and @[extern] in verified modules.
• Read-only specification. Hash Spec.lean and the extracted model in CI; the agent may write only proofs.
• Vacuity and mutation audits. Re-run the satisfiability and mutation checks from the falsification stage in CI, so a specification edited after it passed them cannot slip through.

Here is what the axiom gate looks like as a CI step:

#!/usr/bin/env bash
set -euo pipefail
sha256sum -c spec.sha256                       # spec and extracted model unchanged
if grep -rnE '^\s*(partial|unsafe) def|@\[(implemented_by|extern)' Verified/; then
  echo "escape hatch in verified module"; exit 1
fi
lake env lean ci/Axioms.lean | tee axioms.log  # #print axioms for each theorem
if grep -qE 'sorryAx|trustCompiler' axioms.log; then
  echo "proof depends on a forbidden axiom"; exit 1
fi

What to Do on Monday

Isolate the decision kernel, pick the route by what it is, and verify its call graph from the leaves up. Put the axiom, escape-hatch, and read-only-spec gates into CI before the first proof. Spend your engineers on the specification and its audits, not on the proof script, because the proof is now the cheap part.

14 The Product Landscape

Formal verification is fifty years old, and cost was always the barrier. seL4's functional-correctness proof took about 20 person-years against roughly 2.2 to write the kernel, which is why adoption stayed in avionics, cloud cryptography, and other domains where failure is measured in lives or billions. Two forces are changing that: AI-generated code has outrun human review, and a proof checker gives a model a deterministic pass-or-fail signal, so it can iterate against Lean's kernel or an SMT solver until the proof closes. The same loop that makes proofs searchable makes them cheap enough to sell.

Two Architectural Bets

The vendors below split along one architectural line. The first camp verifies what was written: Truidic, &Truth, Theorem, and Harmonic take C, Rust, Python, Verilog, or compiled binaries and use AI to generate specifications and proofs after the fact. The second camp restricts what can be written: Nectry compiles natural language into NectryCore, a deliberately non-Turing-complete intermediate language, so the compiler can decide every security property at build time. The first camp inherits the specification bottleneck; the second pays in expressiveness, because the customer leaves general-purpose code behind.

Truidic and Nectry show the two bets in concrete form. Madan Musuvathi spent two decades in Microsoft Research's software-reliability group on model checking and systems verification; Truidic sells automated code verification and regulated-industry rule checking into enterprises that will not hire formal-methods PhDs. Adam Chlipala's Ur/Web and Fiat Cryptography work supply Nectry's formal pedigree; NectryCore is the commercial artifact. Because its target language is decidable, Nectry can prove information-flow control (an agent cannot leak PII) and structural agent boundaries (an agent cannot write outside its declared scope or reach the network) as compile-time artifacts rather than prompt guardrails. The trade is stark: Nectry's guarantees hold because the customer writes in Nectry's language, not Python or C.

The Vendors

Figure 3 maps the seven most visible products against founders, proof stack, and target market. Each company gets a full-width band; the three columns compare the rest. Founder and stack data is public; funding figures and customer claims are company or press claims, not independently verified.

The table makes the strategic split visible. Some teams sell a general proof platform and leave the software class to the customer; others sell a vertical product where the specification and the market arrive together. The first group inherits the specification problem; the second inherits the integration problem. Neither has yet made deep functional correctness of unmodified production code routine.

Inside the Products

Figure 3 compares the companies; Figure 4 compares the engineering. Each product gets a full-width band; the five columns are the decisions a team makes when it adopts one: developer input, who writes the specification, how code becomes a mathematical object, what layer the product adds over the prover, and what a failure looks like.

The Strategic Split

The table is not a ranking; it is a map of where each product puts the automation. Theorem and Harmonic automate the two hardest mechanical steps, translation and proof search, and leave the specification to a fuzz harness or an English dialogue. &Truth automates the specification step itself through its Specification Factory. Imandra automates the logic layer by replacing the prover with ImandraX. Raw Lean automates none of it: the engineer rewrites the code, writes the specification, and drives the tactics by hand. That is why its row is the control against which the products are measured.

The choice also determines the failure experience and the trusted surface. Theorem's failures arrive as concrete bug reports or crash inputs from the fuzz harness, and its trusted base is the RISC-V/Linux model plus the translation into Rocq. Harmonic's failures are refutation traces, and its trusted base includes the C/Verilog semantics and the RL-trained lemma agent. &Truth's failures are specification/implementation mismatches, with CSLib and cvc5 underneath. Imandra's are executable counterexamples from ImandraX. The rows are not independent: a product that automates translation inherits the specification bottleneck, one that automates specification still depends on the prover and its library, and one that replaces the prover has to rebuild the ecosystem around it.

15 What Is Proved, What Is Open

To answer the title: what can we verify today? Sort the systems this post has covered by two questions, whether the code was written behind a proof or already existed, and whether the property is shallow and universal or full functional correctness, and the evidence clusters in two corners, with a third nearly empty. Figure 5 maps the results.

New code built behind a proof gate can reach deep properties: seL4, CompCert, Cedar, the Velvet algorithms, partly Eita, and, from the Anthropic appendix, an interpreter for a Python fragment written in Rust and proved with Verus against a formal semantics, with conformance to CPython tested rather than proved. Existing code can be verified at scale, but so far only for shallow properties such as crash-freedom, which is what the Anthropic and Theorem result shows. Deep properties of code nobody wrote with a proof in mind have one completed result, AlphaProof Code's security proofs for libsignal, which had five specialists and a published formal literature behind its specification. Beyond it the ground is still largely empty, with Aeneas-based efforts on SymCrypt and curve25519-dalek the main work in progress.

The Routes Side by Side

Those five routes map onto that picture. Each suits a different kind of software, and each is at a different stage of maturity. Figure 6 is the scorecard.

Read the maturity labels with the trusted-base chips beside them. Every "today" depends on something outside the proof: a reference specification, an ISA model, a lifter, or a human audit.

What Would Change the Answer

16 Conclusions

For most of computing history, source code was the primary artifact, compilers were trusted translators, and tests were a probabilistic check that code roughly matched intent. Formal verification was admired and reserved for flight software and separation kernels, because at half a person-day per line it was economically unthinkable anywhere else.

AI has broken that equilibrium from both sides. Agents flood organizations with code faster than humans can review it, and neural provers paired with a trusted kernel are pulling the cost of a proof from person-months toward compute-hours. But AI does not dissolve the hard problems of formal methods. It relocates them.

Models are excellent abductive engines inside a symbolic loop: they guess invariants, decompose goals, repair from diagnostics, and navigate tactic trees once premise repair and counterexample pruning keep them honest. Asked to translate stateful systems code into Lean in one leap, they fail on most nontrivial benchmarks, invent premises, collapse across function boundaries, trip over dependent types and partial, and will happily prove a vacuous theorem.

Prompting "rewrite my C in Lean and prove it" will not be enough. The teams that win will build deterministic bridges, Aeneas for Rust, Velvet for algorithms, verified lifters for C, Verilog, and binaries, and spend their human attention on the one artifact no machine can validate for them: the specification of what the system is supposed to do. AlphaProof Code is the clearest instance so far: its authors wrote no proof code, and by their own account most of their effort went into the specification.

The commercial landscape now splits along the same line. General proof platforms sell proof search and leave the specification to the customer; vertical products restrict what can be written until the specification is decidable. Both are ways of packaging the bottleneck, and neither removes it.

The proof got cheap. The specification and the bridge from real software to Lean are now the whole game.

References

• Bursuc, S., Ehrenborg, T., Lin, S., et al. (2025). "A benchmark for vericoding: formally verified program synthesis." arXiv:2509.22908. Available at: arxiv.org/abs/2509.22908
• Lin, X., Cao, Q., Huang, Y., Wang, H., Lu, J., Liu, Z., Song, L., Liang, X. (2024). "FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving." NeurIPS 2024 Datasets and Benchmarks. arXiv:2406.14408. Available at: arxiv.org/abs/2406.14408
• Loughridge, C., Sun, Q., Ahrenbach, S., Cassano, F., Sun, C., Sheng, Y., Mudide, A., Misu, M. R. H., Amin, N., Tegmark, M. (2025). "DafnyBench: A Benchmark for Formal Software Verification." Transactions on Machine Learning Research. arXiv:2406.08467. Available at: arxiv.org/abs/2406.08467
• Miranda, B., Daruru, S., Hersch, E. S., Zhou, Z., Nie, A., et al. (2026). "VeriBench: End-to-End Formal Verification Benchmark for AI Coding Agents in Lean 4." Preprint. Available at: cs.stanford.edu
• Thakur, A., Lee, J., Tsoukalas, G., et al. (2025). "CLEVER: A Curated Benchmark for Formally Verified Code Generation." NeurIPS 2025 Datasets and Benchmarks. arXiv:2505.13938. Available at: arxiv.org/abs/2505.13938
• Xu, X., Li, X., Qu, X., Fu, J., Yuan, B. (2025). "Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification" (DafnyComp). arXiv:2509.23061. Available at: arxiv.org/abs/2509.23061
• Ye, Z., Yan, Z., He, J., Kasriel, T., Yang, K., Song, D. (2026). "VERINA: Benchmarking Verifiable Code Generation." ICLR 2026. arXiv:2505.23135. Available at: arxiv.org/abs/2505.23135

• de Moura, L., Ullrich, S. (2021). "The Lean 4 Theorem Prover and Programming Language." CADE 2021, LNCS, 625–635. Available at: doi.org/10.1007/978-3-030-79876-5_37
• de Moura, L. (2026). "Postmortem for Kernel Soundness Bug #14576." Personal blog, August 1, 2026. Available at: leodemoura.github.io
• Limperg, J., From, A. H. (2023). "Aesop: White-Box Best-First Proof Search for Lean." CPP 2023, 253–266. Available at: doi.org/10.1145/3573105.3575671
• Mathlib Community (2026). "Mathlib statistics." Accessed November 7, 2026. Available at: mathlib.org
• Mohamed, A., Mascarenhas, T., Khan, H., et al. (2025). "lean-smt: An SMT Tactic for Discharging Proof Goals in Lean." CAV 2025, LNCS, 197–212. Available at: doi.org/10.1007/978-3-031-98682-6_11

• Gladshtein, V., Pîrlea, G., Zhao, Q., Kurin, V., Sergey, I. (2026). "Foundational Multi-Modal Program Verifiers." PACMPL 10(POPL). Available at: doi.org/10.1145/3776719
• Gladshtein, V., Kurin, V., Feng, Y., Kafle, D., Pîrlea, G., Zhao, Q., Sergey, I. (2026). "Velvet: A Foundational Multi-modal Verifier for Imperative Programs in Lean." CAV 2026, LNCS 16683, 228–242. Available at: doi.org/10.1007/978-3-032-32526-6_11
• Lean FRO (2026). "The mvcgen tactic." Lean Language Reference. Accessed November 7, 2026. Available at: lean-lang.org
• Pîrlea, G., Gladshtein, V., Kinsbruner, E., Zhao, Q., Sergey, I. (2025). "Veil: A Framework for Automated and Interactive Verification of Transition Systems." CAV 2025, LNCS, 26–41. Available at: doi.org/10.1007/978-3-031-98682-6_2

• Achim, T., Best, A., Bietti, A., et al. (2025). "Aristotle: IMO-level Automated Theorem Proving." arXiv:2510.01346. Available at: arxiv.org/abs/2510.01346
• Anthropic (2026). "Learning more about Claude's mathematical capabilities." August 10, 2026. Available at: anthropic.com
• de Moura, L. (2026). "When AI Writes the World's Software, Who Verifies It?" Personal blog, February 28, 2026. Available at: leodemoura.github.io
• He, B., Li, Z., Sun, W., et al. (2026). "Neuro-Symbolic Proof Generation for Scaling Systems Software Verification." OSDI 2026, 2533–2550. Available at: usenix.org
• Hubert, T., Mehta, R., Sartran, L., et al. (2025). "Olympiad-level formal mathematical reasoning with reinforcement learning" (AlphaProof). Nature 651(8106), 607–613. Available at: doi.org/10.1038/s41586-025-09833-y
• Li, Z., Yang, Z., He, D., et al. (2026). "Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification." arXiv:2603.19329. Available at: arxiv.org/abs/2603.19329
• Thompson, K., Saavedra, N., Carrott, P., Fisher, K., Sanchez-Stern, A., Brun, Y., Ferreira, J. F., Lerner, S., First, E. (2025). "Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification." ICSE 2025. Available at: doi.org/10.1109/ICSE55347.2025.00161

• Chen, T., Lu, S., Lu, S., Gong, Y., Yang, C., Li, X., Misu, M. R. H., Yu, H., Duan, N., Cheng, P., Yang, F., Lahiri, S. K., Xie, T., Zhou, L. (2025). "Automated Proof Generation for Rust Code via Self-Evolution" (SAFE). ICLR 2025. arXiv:2410.15756. Available at: arxiv.org/abs/2410.15756
• Feng, Y., Kafle, D., Gladshtein, V., et al. (2026). "Certified Program Synthesis with a Multi-Modal Verifier" (LeetProof). ASE 2026, 3341–3353. Available at: doi.org/10.1145/3832783.3837559
• Mugnier, E., Anaya Gonzalez, E., Polikarpova, N., Jhala, R., Zhou, Y. (2025). "Laurel: Unblocking Automated Verification with Large Language Models." PACMPL 9(OOPSLA1), 1519–1545. Available at: doi.org/10.1145/3720499
• Sevenhuijsen, M., Etemadi, K., Nyberg, M. (2024). "VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models." arXiv:2411.19275. Available at: arxiv.org/abs/2411.19275
• Sun, C., Sheng, Y., Padon, O., Barrett, C. (2024). "Clover: Closed-Loop Verifiable Code Generation." SAIV 2024, LNCS, 134–155. Available at: doi.org/10.1007/978-3-031-65112-0_7
• Wei, R., Zhu, L., Wang, H., et al. (2026). "Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering" (Forge). arXiv:2606.22413. Available at: arxiv.org/abs/2606.22413
• Wu, H., Barrett, C., Narodytska, N. (2024). "Lemur: Integrating Large Language Models in Automated Program Verification." ICLR 2024. Available at: arxiv.org/abs/2310.04870

• Chaudhuri, S., Ferraiuolo, A., Kovsharov, A., et al. (2026). "AlphaProof Code: Verifying Signal's Security at the Machine-Code Level." Google DeepMind technical report, November 10, 2026. Available at: deepmind.google
• Cryspen (2023–2026). "hax: A Rust verification tool." GitHub repository. Available at: github.com/cryspen/hax
• Gäher, L., Sammler, M., Jung, R., Krebbers, R., Dreyer, D. (2024). "RefinedRust: A Type System for High-Assurance Verification of Rust Programs." PACMPL 8(PLDI). Available at: doi.org/10.1145/3656422
• Greenaway, D., Lim, J., Andronick, J., Klein, G. (2014). "Don't Sweat the Small Stuff: Formal Verification of C Code Without the Pain" (AutoCorres). PLDI 2014. Available at: doi.org/10.1145/2594291.2594296
• Ho, S., Protzenko, J. (2022). "Aeneas: Rust Verification by Functional Translation." PACMPL 6(ICFP), 711–741. Available at: doi.org/10.1145/3547647
• Lean FRO and AWS (2024–2026). "LNSym: Native Code Symbolic Simulator in Lean." GitHub repository. Available at: github.com/leanprover/LNSym

• Beneficial AI Foundation (2026). "curve25519-dalek-lean-verify." Project site. Available at: beneficial-ai-foundation.github.io
• Klaus, N. (2026). "From Rust Code to Mathematical Proof: How We Verify Safety-Critical Rust." Runtime Verification blog, May 19, 2026. Available at: runtimeverification.com
• Microsoft Research (2025). "Rewriting SymCrypt in Rust to modernize Microsoft's cryptographic library." Microsoft Research blog, June 10, 2025. Available at: microsoft.com
• Yang, C., Li, X., Misu, M. R. H., Yao, J., Cui, W., Gong, Y., Hawblitzel, C., Lahiri, S., Lorch, J., Lu, S., Yang, F., Zhou, Z., Lu, S. (2025). "AutoVerus: Automated Proof Generation for Rust Code." PACMPL 9(OOPSLA2). Available at: doi.org/10.1145/3763174

• ARIA (2026). "Safeguarded AI." Programme page. Accessed November 7, 2026. Available at: aria.org.uk
• Disselkoen, C., Eline, A., He, S., et al. (2024). "How We Built Cedar: A Verification-Guided Approach." arXiv:2407.01688. Available at: arxiv.org/abs/2407.01688
• Keles, A., Menon, J., Nalla, S., Shah, V. (2026). "Closing the verification loop: Observability-driven harnesses for building with agents." Datadog blog, March 9, 2026. Available at: datadoghq.com
• Lucas, K., Lynch, A., Tong, L., et al. (2026). "LLMs are making formal software verification feasible at a much larger scale." Anthropic Research (Frontier Red Team, with Theorem), October 22, 2026. Available at: anthropic.com; appendix: PDF
• Zamaraiev, V. (2026). "Eita: an EVM specified in Lean 4." Project site. Available at: eita.run
• Zamaraiev, V. (2026). "How it's verified: what is proved, what is checked, what is trusted." Project site. Available at: eita.run/verified
• Zamaraiev, V. (2026). "eita-evm: an EVM specified in Lean 4, with native handlers emitted from the spec." GitHub repository. Available at: github.com/valeryz/eita-evm

• Ethereum Foundation (2026). "Ethereum Execution Layer Specification (EELS)." Executable Python specification, GitHub repository. Accessed November 10, 2026. Available at: github.com/ethereum/execution-specs
• Harmonic (2026). "Aristotle Expands Into Formal Verification for Software and Hardware, Starting With C and Verilog." October 27, 2026. Available at: harmonic.fun
• Harmonic (2026). "Formally Verifying the MUL and DIV Instructions of the Ibex RISC-V CPU Using Aristotle." November 3, 2026. Available at: harmonic.fun
• Harmonic (2026). "Speed up your code without wondering what you broke." LibTomMath case study. Available at: harmonic.fun
• Harmonic (2026). "Tensordyne's most complex block and early exploration for its next chip." Case study. Available at: harmonic.fun
• Lazaropoulos, L., Paraskevopoulou, Z. (2026). "Foundational Refinement Proofs for EVM Bytecode, at the Price of Tokens." arXiv:2607.26306. Available at: arxiv.org/abs/2607.26306
• Nethermind (2026). "How We Formalized Ethereum Execution: A Trustworthy Semantics of the EVM and Yul in Lean for Cancun." Nethermind blog, February 6, 2026. Available at: nethermind.io

• Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., Trippel, C. (2023). "nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models." CAV 2023, LNCS, 383–396. Available at: doi.org/10.1007/978-3-031-37703-7_18
• Dickson, A. (2024). "Limitations on Formal Verification for AI Safety." AI Alignment Forum, August 19, 2024. Available at: alignmentforum.org
• Kleppmann, M. (2025). "Prediction: AI will make formal verification go mainstream." Personal blog, December 8, 2025. Available at: martin.kleppmann.com
• Lahiri, S. K. (2024). "Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages." FMCAD 2024. Available at: arxiv.org/abs/2406.09757
• Sosso, A., Arora, A., Spitters, B. (2026). "Isomorphism Is Not Enough: An Agentic Audit of Verified Code Generation in Lean." arXiv:2605.23772. Available at: arxiv.org/abs/2605.23772
• Zaliva, V. (2026). "Keeping the Human in the Loop: A Principled Approach to Verified AI-Generated Code." Preprint, 28 October 2026. Available at: zaliva.org
• Zhong, Z., Raghunathan, A., Carlini, N. (2026). "ImpossibleBench: Measuring LLMs' Propensity of Exploiting Test Cases." ICLR 2026. arXiv:2510.20270. Available at: arxiv.org/abs/2510.20270

• Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A. (2019). "Simple High-Level Code for Cryptographic Arithmetic – With Proofs, Without Compromises." IEEE Symposium on Security and Privacy 2019. Available at: doi.org/10.1109/SP.2019.00005
• Klein, G., Elphinstone, K., Heiser, G., et al. (2009). "seL4: Formal Verification of an OS Kernel." SOSP 2009, 207–220. Available at: sigops.org
• Leroy, X. (2009). "Formal Verification of a Realistic Compiler." Communications of the ACM 52(7), 107–115. Available at: doi.org/10.1145/1538788.1538814
• NIST National Vulnerability Database (2014). "CVE-2014-0160 (Heartbleed)." Available at: nvd.nist.gov

• The SaaS News (2026). "&Truth Raises $70M Seed." November 2, 2026; press coverage only, no primary company source checked. Available at: thesaasnews.com