AI now writes machine-checked proofs at a scale nobody expected, and you should use them. A proof tells you the code matches the spec. We tell you whether the spec matches the business, and whether your tests would notice when either one moves.
The News
On 2026-10-22, Anthropic's Frontier Red Team and Theorem published LLMs are making formal software verification feasible at a much larger scale. Claude proved 239 fuzz entry points across 123 OSS-Fuzz libraries crash-free for every input under 64 MB: no fuzz-test failure and no AddressSanitizer crash. The proofs are checked in Rocq against the compiled RISC-V binary and run to about 180 million lines. Hundreds of bugs were found on the way, among them a rediscovered libexpat CVE. (Source: Anthropic and its PDF appendix, verified 2026-10-23.)
Theorem now offers the pipeline free to qualifying open-source projects through OSS Verify: Rocq proofs that a fuzz target never crashes on any input up to 64 MiB, enrolment by pull request, bugs disclosed privately. (Source: Theorem OSS Verify, verified 2026-10-23.)
That is a real result. Memory safety of real C libraries is provable at scale. If you ship a parser, a codec or a protocol library, put it through a prover. The same holds across formal verification's home ground: concurrency and distributed-protocol design, properties over infinite domains, crypto, compilers and kernels. The AI proof companies working that ground are complements to what we do, and their results are evidence we carry.
Read the Spec
Read how the spec was written. The authors say it directly: "The difficulty of obtaining a comprehensive and unambiguous spec is a significant obstacle to verifying software at a larger scale". So they took "the approach of automatically converting their preexisting compilable test suites into a spec": do not crash, plus the fuzz harness's own assertions.
Their limits section names what remains, in their words:
Two more findings from the same work matter to every engineering team. Reward hacking is real: "Claude could make any theorem provable by rewriting the program into one that trivially never crashes", so patches were penalized and audited. And in a companion experiment in the appendix, on a verified interpreter, tests and proofs were measured against each other: "we deliberately injected seven bugs … Five survived the random tests, while all seven broke the proof". Seeded faults, scored. That is mutation analysis, and it is exactly how you grade a spec that was made from tests. (Source: Anthropic and its PDF appendix, verified 2026-10-23.)
The full walkthrough is in our post Claude proved 123 libraries crash-free. Here's what still needs checking.
The Spec Problem
The property the AI proofs established at scale is one every program shares: do not crash. The software an enterprise ships is different. Its spec is the requirements, the acceptance tests and the business rules: the rate book, the eligibility matrix, the order lifecycle, the refund policy. Nobody holds those as a formal theorem. Mike Dodds of Galois puts it plainly in Specifications Don't Exist: “we don’t have a formal specification for Chrome, or a word processor”, and with cheap proofs “we will quickly verify every compiler and microkernel, then find that we’re stuck.” (Source: Galois, 2025-06-16, verified 2026-10-23.) Martin Kleppmann, who predicts formal verification goes mainstream, says the same: "the challenge will move to correctly defining the specification". (Source: Kleppmann, December 2025, verified 2026-09-25.)
What a release of business software is made of, HTTP and API behaviour, database-backed workflows, auth, UI and third-party integrations, appears in no AI formal-verification result we found. (Public results searched 2026-10-23; each targets parsers, kernels, crypto, compilers, smart contracts, circuits or math.) The nearest requirements bridge, Kiro's property tests generated from EARS requirements, describes itself this way: "It provides evidence of correctness, not a proof. It is not formal verification …" (Source: Kiro correctness docs, verified 2026-10-23.) Using Kiro? See Karate for Kiro.
So the question that decides a business-software release is the one the proof's authors left open: does the spec match the business? That is the layer Karate governs. Requirements are joined to the tests that claim them. Business rules are executable, and they are the oracle. Tests are graded on whether they would notice a defect. AI-written work is marked until a human reviews it. Roadmap And every verdict lands on a requirement, in one git-native graph that your agent drives and a human audits.
Property by Property
A temporal-logic proof speaks about one behaviour of one model at a time. Hillel Wayne, author of Practical TLA+, draws that boundary in What TLA+ can and can't check and calls the workarounds "useful hacks, but they're still hacks" (verified 2026-10-23). A business-software release turns on comparisons: the model and the running service, the mock and the provider, this version and the last, the suite and its mutants. Comparing two running systems, two versions, or a suite against its mutants is evidence we run, not a formula anyone proves. Here is each property class, its formal home, what Karate runs for it, and the claim on the report.
| Property | Its formal home | What Karate runs | The claim on the report |
|---|---|---|---|
| Invariant: "the premium is never below base" | TLA+ and TLC, Lean, Dafny | Rulebook guarantees, hunted at the corners of the declared input domain; lifecycle twin walks | Proven for this input domain when the domain is fully enumerated or certified; sampled otherwise, with the cause named |
| Reachable: "a quote can be bound" | TLC's REACHABLE check; CTL | Reachability over the declared domain and the lifecycle walk | Reachable, with the input or sequence that reaches it; over a closed domain, not reachable, proven for this input domain |
| Enabled at each state | CTL | The guard census over every walked state | Which moves are enabled at each walked state, within declared ceilings |
| Model vs implementation | Refinement proofs; trace validation, which its authors say "does not provide formal correctness guarantees" (Cirstea, Kuppe, Loillier, Merz, SEFM 2024, verified 2026-10-23) | The model replayed against the live service; the paired run against mock and provider | A measured divergence set, every disagreement named |
| Across versions | Regression verification, undecidable in general | The silent-drift audit against a blessed baseline | Meaning moved, with the word-level diff |
| Would the suite notice | Mutant killing formalized as a hyperproperty (Fellner et al., SEFM 2019); no prover ships it | Mutation testing over the rulebook, the live responses and the twin's guards | Assertion strength, scored, survivors named |
| Statistical: p95, pass rate | Statistical model checking | Statistical gates over N samples Roadmap | A gate on the measured rate |
| Not formalizable: "quotes are easy to compare" | None | A prose requirement joined to graded evidence and human review | A verdict carrying its evidence grade |
The industrial record agrees. AWS's Cedar team found 4 bugs while writing proofs, and 21 more by differential and property-based testing around the verified model (arXiv 2407.01688, verified 2026-09-25). Proof and testing, each where it is strongest.
Four Engines
Four engines grade the spec you actually have. They run in one self-hosted JAR, driven by your own LLM over MCP or curl, with no model in the verdict.
Your rate book, eligibility and pricing logic live in one rulebook: the spec the business reads, the oracle that computes every expected answer, and the mock's brain. A guarantee such as "the discount never exceeds the cap" names the requirement it defends. A violation turns that requirement FAILING and the release NOT READY, with the smallest breaking input attached.
Business rules testing →Boundary, equivalence-class and pairwise decks are generated from the rules: every pair of input values by default, every triple and beyond on demand. Every row carries the computed expected result, the audit trail and the requirement it exercises.
Test data generation →The lifecycle twin walks every command order under declared ceilings, constructs the long orders no shortest route reaches, and replays its witnesses against the live system. A refusal given for the wrong reason is its own finding. A TLC counterexample becomes a sequence on the twin and replays against the running service on every commit.
Defects are seeded into the rulebook, the twin's guards or the live responses, never your source. Your suite replays, and every survivor comes back naming the criterion nobody defends. Assertions copied from observed output cannot inflate the score. When tests become the spec, this is the grade of the spec.
API mutation testing →And meaning drift is caught under a green suite: an output, a decision, a guarantee or a refusal that moved with no example edited is reported against a blessed baseline.
Bring Your Proofs
Keep your provers. Connect them to the release. Run the prover your way; we carry the result, in the prover's own words.
Shipped
Hand a TLC model-checking result to Rule.prove and it lands on the acceptance criterion it argues for, as model evidence. A counterexample fails that criterion, an edited spec or model marks it stale, and a project can block any release that is missing a proof. The link between your spec and your code is recorded as asserted, with the person who asserted it named.
A Rocq, Lean, Verus or Dafny result lands on its criterion, bound to the theorem statement and to the code it was about, source tree or binary. It stops counting when the theorem or the code moves, and is re-attested when only the proof body changes. Alloy results join the same lane.
The output of Print Assumptions, #print axioms or dafny audit travels with the proof, captured verbatim, and the scope is rendered as the domain the theorem covers. The spec your proof stands on carries its own grade from your seeded-fault run: faults seeded, faults caught.
The one thing a proof checker cannot check is a release gate here. An AI-written theorem statement or proof mapping is unreviewed AI work, and on a high-criticality requirement it blocks the release until a human signs it off.
A guarantee that turned green because the rules now refuse more input, or because its assertion was rewritten, is named and never credited. For an ingested proof, the theorem and the code moving in the same change is the same finding. It is the reward hacking the proofs-at-scale team audited by hand, caught by the engine on every run.
Finite Domains
Rating, pricing and eligibility cores have finite, piecewise-constant input domains, and over a domain like that, exhaustive enumeration is the proof. ISO/IEC/IEEE 29119-1 says "It is impossible to test a software system exhaustively, thus testing is a sampling activity." Over a closed, finite input domain, it does not have to be.
When a guarantee's input domain is finite and fully enumerated, the verdict reads proven for this input domain. Anything less reads sampled, and the report names what stopped it: an unbounded number, free text, the inside of a list.
A domain too large to enumerate is certified once and stored beside the rulebook, so every later check reads proven for this input domain, with the rows the rules themselves refuse subtracted from the claim.
The certificate rests on one checker over rules in a declared total dialect. The split tree is exported beside it, so a third party rechecks the partition and reads the figures back off the leaves.
A situation the requirements promise but the rules make impossible fails its requirement: not reachable, proven for this input domain.
The checker behind every "proven for this input domain" is itself mutation-graded: planted soundness bugs against its own gate, reported as how many it caught.
A guarantee whose premise no input satisfies reads not checked, never green. Certificates over list-valued inputs join the same engine.
See it: the fleetquote rating rule analysis, Rule Check tab. The fleetquote and policy-api rating rulebooks carry certificates.
For Auditors
Every claim behind a release verdict, in one document an auditor reads: its evidence grade, its input domain, the trusted base and tool version, every disclosure, the proofs attached with the assumptions they rest on, and which AI-authored work nobody has reviewed.
The graph underneath it runs today. The traceability matrix is computed from what actually ran. Every item is graded exercised, partly exercised, incidental or not exercised. When an AI run ticks off a requirement, the report shows it as an AI claim, graded below captured evidence, so an agent never quietly marks its own work verified. The verdict is computed by versioned code with no model in the path, and it reproduces from the same inputs. How the release verdict works →
Regulators ask for exactly this evidence. The NAIC AI model bulletin (2023) asks for testing, "reproducibility, traceability, model drift" and auditability.
Why this matters more as AI writes more of the code: AI verification debt, and why cheap proofs move the bottleneck to the spec.
Public Proof
In the public fleetquote kit, a TLA+ model of the quote lifecycle sits beside its executable twin. TLC checks the model and finds no error. A planted defect lives in the service code, and the lifecycle twin catches it against the running service. TLC flags the same invariant, ApprovedNeverBindsAfterExpiry, only in a weakened copy of the spec where a modeller wrote the defect into the model. The design proof and the shipped-code check do different jobs. You want both, landing on the same requirement.
proofs/rating
TLC: no error found
proofs/rating-weakened
TLC: ApprovedNeverBindsAfterExpiry violated
Twin vs live service: planted defect caught
rating and rating-weakened, with their TLC output.
NOT READY on RATE-001, with the breaking input.
An agent-written rulebook and lifecycle model find the five bugs an InfoQ article seeds into a published meeting scheduler, with every branch's verification record published.
FAQ
No. A proof checks code against a spec; tests and rules are where the spec comes from. In Anthropic and Theorem's proofs-at-scale result, the team converted existing test suites into the spec, and wrote that "a proof checker can’t tell you whether your spec matches reality". Use provers where they are strongest, and grade the spec they stand on. A proof tells you the code matches the spec. We tell you whether the spec matches the business, and whether your tests would notice when either one moves.
That 239 fuzz entry points across 123 OSS-Fuzz libraries never crash, ASan-crash-free, for every input under 64 MB, checked in Rocq against the compiled RISC-V binary. The spec was crash-freedom plus the fuzz harness's own assertions. Source: anthropic.com/research/formal-verification, 2026-10-22, verified 2026-10-23.
No. Keep them. Today a TLC model-checking result lands on the acceptance criterion it argues for, a counterexample fails it, and a project can block any release missing a proof. Rocq, Lean, Verus and Dafny results bound to their theorem statement and code, with the prover's assumptions report captured verbatim, are on our roadmap. Roadmap We carry the result; the claim stays the prover's.
Every input in a declared finite domain was checked and the guarantee held, with the domain printed on the report. A domain too large to walk, up to a billion rows, is certified once and rechecked on every later run. Anything less reads sampled, with the reason named. Rating, pricing and eligibility logic is exactly this shape.
A person, and the release gate counts it. An AI-written theorem statement or proof mapping is unreviewed AI work, and on a high-criticality requirement it blocks the release until a human signs it off. This gate is on our roadmap; today an AI run's claims already read as AI claims, graded below captured evidence.
A guarantee that turned green because the rules started refusing more input, or because its assertion was rewritten, rather than because the behaviour got right. The proofs-at-scale team named the same pattern: a theorem made provable by rewriting the program into one that never crashes. Karate reports it as a finding against the blessed baseline and never credits it. This check is on our roadmap.
No, they are complements. They prove code against a spec; we govern whether that spec matches the business and whether the tests behind it would notice a defect. Their results are evidence our graph carries, on the requirement they argue for.
It produces the evidence they ask for: testing, traceability, reproducibility and drift monitoring, in one record per requirement, computed with no model in the path and reproducible from the same inputs. An assurance dossier per requirement is on our roadmap.
Bring one rulebook and one proof. Leave with a release verdict, graded. Need a proof format or a property class we don't list? We build it during your evaluation.