Pangram verdict · v3.3
We believe that this document is a mix of AI-generated, AI-assisted, and human-written content
AI likelihood · overall
MixedArticle text · 1,585 words · 5 segments analyzed
The Wayback Machine - http://web.archive.org/web/20260629172017/https://queue.acm.org/detail.cfm?id=3819084
June 22, 2026Volume 24, issue 3
What can you confidently guarantee about your software? Fernanda Graciolli and Nada Amin The cost and tooling of formal verification have reached the point of widespread use. By eliminating the cost of writing proofs, AI is removing the biggest barrier to formal verification. This makes it easier than ever to build software with critical business rules that are guaranteed to be mathematically correct, rather than merely tested. If your program has a complex set of business rules, can you guarantee that no combination of valid inputs will produce an invalid outcome? Consider a secrets-management platform with a permission system. Rules control who can read, edit, or delete secrets across environments. When a user creates a custom role, the system checks that the new role’s permissions are a subset of the user’s own (i.e., you shouldn’t be able to grant access you don’t have). The boundary check covers every combination of permission operators. It has a thorough test suite, and all are passing. But there’s a case that the tests never tried: A user with access scoped to a single environment (say, QA) could create a role scoped to “not development.” That sounds narrow, but “not development” matches every environment except development (e.g., user acceptance testing, sandbox, canary, production, etc.)—meaning a single-environment permission escalated to near-universal access. The boundary check approves it and the tests don’t catch it, because every test uses overlapping values, which means the excluded value always appears in the parent’s set. The bug triggers only when they don’t overlap. A correctly designed and implemented permission system has one fundamental semantic invariant: Permission derivation is subset invariant. That is, the set of environments that a derived permission matches must always be a subset of the environments the granting permission matches. That property says nothing about how permissions are represented. It covers finite sets, negated sets, and any representation that might be added later.
With this invariant set, permission derivation can’t fail at runtime because a bug of this class would be made impossible by construction. The distinction between “the code didn’t fail at runtime” and “the code can’t fail” is what this article is about. What Formal Verification Actually Is At its core, formal verification is a simple concept. You start with properties you want your code to uphold. These are contracts for input and output, functions and methods. For a shopping cart, you might want to prove the following: – The balance never goes negative. – Every item in the cart is reflected in the total. – Only one coupon code can be applied per order. A verifier can’t work with English, so those properties need to be expressed in a verification-aware language—a programming language designed so that specifications and proofs are treated as first-class citizens alongside implementation code. Several exist, each with different strengths: Dafny uses an imperative style familiar to most developers and automates much of the proof work via SMT (satisfiability modulo theories) solvers; Lean has roots in pure mathematics and is rapidly gaining traction for both theorem proving and verified software; Rocq (formerly Coq) and Isabelle are interactive proof assistants with decades of use in research and high-assurance systems; F* targets verified systems programming with extraction to C and OCaml; and TLA+ focuses on specifying and model checking distributed protocols. They all work differently, but the core idea is the same: You write your code and your properties in the same system, and the tool checks that one satisfies the other. Here’s what that looks like in Dafny. For “the balance never goes negative” property, you would write: method ApplyCoupon(balance: int, discount: int) returns (newBalance: int) requires discount >= 0 requires balance >= discount ensures newBalance >= 0{ newBalance := balance - discount;} The requires clauses are preconditions, which means that this must be true before the function runs. The ensures clause is a postcondition; this is what the function guarantees when it finishes. The verifier doesn’t run this code. Instead, it reasons about its structure and hands the verification conditions to an automated oracle (in this case, an SMT solver) that determines whether the postcondition holds for every input that satisfies the preconditions.
If it does, the proof goes through. If there’s even one reachable state where the property breaks, the code doesn’t compile. The guarantee is only as good as the spec, but when the spec is right, the guarantee is absolute: The property holds in every reachable state of the program. You can now guarantee that this verified piece of code will not break under any circumstance (that is, assuming preconditions are met, postconditions are ensured). This is fundamentally different from testing. With property tests, you can sample one million random inputs into a system and catch some nasty bugs. Your software sits in production with high confidence levels until a user runs a sequence that would have been caught by the 1,000,001st random input. Verification tells you, “There is no bug to find here.” That 1,000,001st sequence was already covered before the code compiled, and so was every sequence after it. The proof didn’t check them one by one—it ruled them all out at once. So, why haven’t you used it? Because, historically, the cost of writing proofs dwarfed the cost of writing the code. You would state an “obvious” property and then spend days coaxing a proof assistant into accepting it. The tools were slow, the process was painstakingly tedious and required Ph.D.-level skill, and this all produced error messages that were inscrutable. The guarantee was real, but the price was too high, which is why formal verification lived almost exclusively in avionics, chip design, nuclear systems, and cryptographic protocols—domains where a bug costs lives or fortunes. For everyone else, the reasonable conclusion was: Tests are good enough. Now, Formal Verification Is AI’s Problem The conclusion that testing is enough no longer holds because AI can now handle the exact bottleneck that prevented this system from being used in mainstream development in the first place. The bottleneck was not the verification itself since a lot of the tools can check proofs automatically. The bottleneck had to do with writing the proofs: translating an intuitive requirement into the precise logical form a verifier demands, and then spending hours or days wrestling with it when the solver can’t automatically confirm what you know to be true. That’s the part that made the cost prohibitive.
Since Opus 4.5, most frontier LLMs can draft formal specifications from natural-language requirements, propose proof strategies, and—critically—iterate relatively fast on failing lemmas in a tight loop with the verifier. AI proposes implementation candidates, and a deterministic, mechanical process checks each candidate’s correctness. If the proof is wrong, the verifier rejects it and AI tries again. Trust in AI is reduced (to the specifications) because the verifier is an external authority. The human stays in the loop for the part that requires judgment: deciding which properties are worth guaranteeing and system design. Meanwhile, the machine handles the labor of producing a verifiably correct implementation. This changes who and what formal verification is for. It’s no longer just for safety-critical systems with the budget for specialized proof engineers. It’s for anyone who has a property worth proving. Formal Verification in Practice Consider an e-commerce order that follows a state machine: Cart → Placed → Shipping → Delivered, with Cancelled reachable from Placed or Shipping. Placing an order charges the customer’s card; the warehouse begins shipping items; and at any point before delivery, the customer can cancel and the system must issue a refund. The fundamental property to verify is financial conservation: On cancellation, the refund equals exactly the value of unshipped items. Equivalently, the net amount the customer pays must always equal the value of the items they receive. In Dafny: datatype State = Cart | Placed | Shipping | Delivered | Cancelleddatatype Item = Item(name: string, price: nat)datatype Order = Order(state: State, items: seq<Item>, shippedValue: nat, charged: nat, refunded: nat)predicate Valid(o: Order){ o.shippedValue <= Total(o.items) && match o.state case Cancelled => o.charged == Total(o.items) && o.refunded == o.charged - o.shippedValue // ... other states} The critical clause: in Cancelled, refunded == charged - shippedValue. One line encodes the financial conservation law for every possible cancellation: nothing shipped, half shipped, or all but one shipped.
The invariant covers every case at once. Each state transition is a method with preconditions and postconditions: method CancelOrder(o: Order) returns (o': Order) requires Valid(o) requires o.state == Placed || o.state == Shipping ensures Valid(o') && o'.state == Cancelled{ var refund := Total(o.items) - o.shippedValue; o' := o.(state := Cancelled, refunded := refund);} Every state transition preserves Valid. A subsequent FinanciallySound ghost predicate stating that the customer pays for exactly what they received (charged - refunded == shippedValue) discharges automatically from Valid’s Cancelled case. So does a NoMoneyLost lemma: If a charge exists, then either items shipped, a refund was issued, or the order is still in fulfillment. No sequence of operations—adding items, placing, shipping, cancelling—can produce an invalid order. The cancellation refund equals exactly the value of unshipped items. These guarantees hold for every possible order at any price, shipment pattern, and cancellation timing. Catching Drift and Preserving Intent When the accounting is simple, the FinanciallySound property holds up trivially for terminal states Cancelled and Delivered. An engineer with some knowledge of the e-commerce domain, however, knows that features such as discounts, batched and recurring orders, or return windows can add complexity to the accounting.