Formal Verification for AI Agents: How to Prove Agent Output Is Safe

Formal verification is a way to validate AI agent output with a proof instead of a test. A test checks the output for a few inputs. A proof shows that the code obeys a rule for every input that the rules allow. The agent proposes an action, a small deterministic function decides, and a solver proves that the function follows the business rules.

Proofs used to be too expensive for most software. AI agents lower that cost, and they also produce more code and actions that need checks. In June 2026 the trading firm Jane Street announced a formal methods team for these two reasons. Below are simple examples, a working proof for an AI refund agent, and the companies that use formal verification today.

What Formal Verification Means

Software teams check code in three common ways:

Four terms appear in the rest of this post:

• A specification (or spec) is the exact rule that the code must obey.
• A solver is a program that searches for values that make a set of conditions true. Z3, from Microsoft Research, is a solver.
• A proof assistant, such as Lean, checks each step of a proof that a person or an AI writes.
• A counterexample is an allowed input that breaks a rule.

The main difference is "some" versus "all". A test says, "for these 50 inputs, the answer was correct." A proof says, "no allowed input breaks this rule." Yaron Minsky of Jane Street calls this the "∀" (for all) guarantee.

A Working Example: An AI Refund Agent

The refund example shows the full method: write a rule, find a failure, and prove a fix.

An AI agent reads the customer's message and proposes a refund amount. A small approval function checks each amount that the agent requests. Z3 checks the approval function. The AI does not decide if its own answer is safe.

The rules (the specification)

All amounts are in cents. The payment system supplies four trusted values:

• the amount paid
• the amount already refunded
• the per-request limit
• whether the requester has permission to refund this payment

A request is eligible only if all of these are true:

1. The requester has permission to refund this payment.
2. The requested amount is more than zero.
3. The requested amount is not more than the money that remains (paid minus already refunded).
4. The requested amount is not more than the per-request limit.

If the request is eligible, approve the exact amount. If not, approve zero.

The code and the proof

Below are two versions of the approval function. The buggy version forgets money that was already refunded. The functions build math expressions for Z3. They do not call a payment service.

Four parts of the code are new for most readers:

• Ints makes symbols for amounts. Each symbol stands for any integer, not one test value.
• And means that every condition must be true.
• If picks the approved amount: the request if it is eligible, otherwise 0.
• Not(rule) asks Z3 to find a case where the rule is false.

# pip install z3-solver
from z3 import Ints, Bool, If, And, Not, Solver, sat, unsat

paid, refunded, requested, limit = Ints("paid refunded requested limit")
authorized = Bool("authorized")

# What the payment system guarantees about its own data (all amounts in cents).
valid_ledger = And(paid >= 0, refunded >= 0, refunded <= paid, limit >= 0)

def buggy(paid, refunded, requested, limit, authorized):
    ok = And(authorized, requested > 0, requested <= paid, requested <= limit)
    return If(ok, requested, 0)

def fixed(paid, refunded, requested, limit, authorized):
    ok = And(authorized, requested > 0,
             requested <= paid - refunded, requested <= limit)
    return If(ok, requested, 0)

for policy in (buggy, fixed):
    approved = policy(paid, refunded, requested, limit, authorized)
    rule = refunded + approved <= paid      # never refund more than was paid
    s = Solver()
    s.add(valid_ledger, Not(rule))          # search for ANY input that breaks the rule
    result = s.check()
    if result == sat:
        print(policy.__name__, "BROKEN:", s.model())
    elif result == unsat:
        print(policy.__name__, "PROVED: no input breaks the rule")
    else:
        print(policy.__name__, "UNKNOWN:", s.reason_unknown())

Z3 gives one of three answers. sat means "I found an input that breaks the rule." unsat means "no such input exists." unknown means "I could not decide." Treat unknown as a failure, never as a pass.

This is the output from Z3 5.3.2:

buggy BROKEN: [authorized = True,
 paid = 1,
 refunded = 1,
 limit = 1,
 requested = 1]
fixed PROVED: no input breaks the rule

Read the counterexample like this:

1. The customer paid 1 cent.
2. The customer already got 1 cent back.
3. The customer asks for 1 more cent.
4. The buggy function approves it. Total refunds are 2 cents on a 1-cent payment.

Z3 did not test many inputs to find this. It solved the conditions as math. Z3 found a counterexample for the buggy policy. It found none for the fixed policy, for any amounts that valid_ledger allows. The integers in this model have no upper limit, so the proof covers 1 cent and $1,000,000 the same way.

The same bug at a normal size: the customer paid $100, already got $80 back, and asks for $50. The limit is $500. The buggy function approves $50. The fixed function approves $0. It does not cut the request to $20, because the spec says "exact amount or zero".

All results

The script above checks one rule. The full script, at the end of this section, checks five rules for three versions of the function, plus two cases where two workers run at the same time. The five rules are:

1. Never refund more than was paid.
2. No refund without permission.
3. Respect the per-request limit.
4. Approve every eligible request.
5. Approve zero for every ineligible request.

The "deny everything" function always returns zero. It never over-refunds, and it is useless. Rule 4 catches it. A spec needs rules about what the code must do, not only about what it must not do.

The race condition shows a limit of the function itself. The fixed function is correct for one request at a time. Two workers that each read the same old balance can both approve a refund. The system must check the balance and update it as one protected operation. For example, it can lock the payment record until the transaction ends.

"""Formal verification demo: prove rules about a refund approval function with Z3.

Run:
    pip install z3-solver
    python refund_proof.py
"""
from z3 import IntVal, Ints, Bool, If, And, Not, Implies, Solver, sat, unsat

# Symbols, not test values: each one stands for ANY integer (amounts in cents).
paid, refunded, requested, limit = Ints("paid refunded requested limit")
authorized = Bool("authorized")

# What the payment system guarantees about its own data.
valid_ledger = And(paid >= 0, refunded >= 0, refunded <= paid, limit >= 0)


def eligible(paid, refunded, requested, limit, authorized):
    return And(authorized, requested > 0,
               requested <= paid - refunded, requested <= limit)


# Three versions of the approval function, written as Z3 expressions.

def buggy(paid, refunded, requested, limit, authorized):
    # Forgets money that was already refunded.
    ok = And(authorized, requested > 0, requested <= paid, requested <= limit)
    return If(ok, requested, 0)


def fixed(paid, refunded, requested, limit, authorized):
    return If(eligible(paid, refunded, requested, limit, authorized), requested, 0)


def deny_everything(paid, refunded, requested, limit, authorized):
    return IntVal(0)


def show(model, names):
    return {str(v): model.eval(v, model_completion=True) for v in names}


def prove(solver_facts, rule):
    """Search for any input that breaks the rule. Return (result, model)."""
    s = Solver()
    s.add(*solver_facts, Not(rule))
    result = s.check()
    return result, (s.model() if result == sat else None), s


def report(label, result, model, solver, names):
    if result == unsat:
        print(f"  PROVED   {label}")
    elif result == sat:
        print(f"  BROKEN   {label}  counterexample={show(model, names)}")
    else:
        print(f"  UNKNOWN  {label}  reason={solver.reason_unknown()}")
    return result == unsat


def check(name, policy):
    approved = policy(paid, refunded, requested, limit, authorized)
    ok = eligible(paid, refunded, requested, limit, authorized)
    rules = {
        "never refund more than was paid": refunded + approved <= paid,
        "no refund without permission": Implies(Not(authorized), approved == 0),
        "respect the per-request limit": approved <= limit,
        "approve every eligible request": Implies(ok, approved == requested),
        "approve zero for every ineligible request": Implies(Not(ok), approved == 0),
    }
    print(f"== {name}")
    names = (paid, refunded, requested, limit, authorized)
    return all([report(label, *prove([valid_ledger], rule), names)
                for label, rule in rules.items()])


def concurrency():
    r1, r2 = Ints("first_request second_request")
    names = (paid, refunded, r1, r2, limit)
    a1 = fixed(paid, refunded, r1, limit, authorized)

    print("== two workers read the same old balance")
    a2_stale = fixed(paid, refunded, r2, limit, authorized)
    report("never refund more than was paid",
           *prove([valid_ledger], refunded + a1 + a2_stale <= paid), names)

    print("== second worker sees the first update")
    a2_serial = fixed(paid, refunded + a1, r2, limit, authorized)
    report("never refund more than was paid",
           *prove([valid_ledger], refunded + a1 + a2_serial <= paid), names)


if __name__ == "__main__":
    for name, policy in [("buggy", buggy), ("fixed", fixed),
                         ("deny_everything", deny_everything)]:
        check(name, policy)
    concurrency()

What a Proof Does Not Cover

The refund proof depends on the specification, the input assumptions, and the model. Each one is a place where a real system can still fail.

The spec can be wrong. The proof checks the code against the rules that you wrote. If the business wants a daily limit per customer and the spec says "per request", the proof passes and the product is wrong. A Microsoft Research paper, Evaluating LLM-driven User-Intent Formalization, says there is "no algorithmic way" to confirm that a spec matches what the user wants. A person must review the spec.

The inputs must be trusted. The proof assumes that the paid amount, earlier refunds, and permission come from the payment system. If the model or the customer can supply these values, the proof does not protect you.

The proof covers the approval function, not the reply. Some reply rules are exact, such as a required field or an allowed value. A complete rule for "a helpful and correct reply" is much harder to write. Proofs work best on the small deterministic core: limits, permissions, and money math.

The model of the code must match the real code. In this example, the policy is written as Z3 expressions. If production runs separate Python or Java code, you must also check that the production code follows the same rules after each change.

Retries, payments, and databases need their own work. Duplicate requests, payment API failures, and transactions are outside this proof.

Types: The Formal Method Most Teams Already Use

A static type checker checks code before it runs. It rejects operations that break the language's type rules. This is a small, automatic proof. Minsky gave two examples in his Bug Bash 2026 talk.

Example 1: cross-site scripting (XSS). XSS happens when a browser runs attacker-controlled content as code in a page. In Jane Street's web framework, page content must have the type "HTML node". A plain string is a different type. Node.text turns a string into escaped text, which the browser shows but does not run. If a developer passes a plain string where an HTML node must go, the code does not compile. This blocks that path to XSS everywhere in the codebase, as long as the code does not bypass the interface.

Example 2: "make illegal states unrepresentable". Minsky showed a network switch configuration. The first design stored a list of commands, such as "set MTU", "shut down", and "add IP address". MTU (maximum transmission unit) is the largest packet size allowed on the interface, in bytes. The command list can set the MTU two times with two different values. The code that reads the list must then guess which value is correct.

The better design is a record with one field for each setting:

• MTU: optional, so zero or one value.
• Shut down: one true or false value.
• IP addresses: a list, because many are allowed.

With this design, two MTU values cannot exist. The code that reads the config gets simpler, and that class of bug cannot occur.

Basic types separate kinds of values, such as numbers and text. Advanced types, such as refinement types, can also state rules about values, for example "an integer from 0 to 100". The refund rule depends on several values together, so the example above uses Z3.

The Cost of Formal Verification

Jane Street has used OCaml, a typed functional programming language, for many years. It still said no to full formal methods. In the talk, Minsky said he spent years "disappointing people" at conferences with that answer. The reason was cost.

The standard example is seL4, a small operating system kernel. Its proof shows that the C code follows a formal spec. The original seL4 paper (SOSP 2009) gives these numbers. One person-year is one person working for one year.

Minsky's post adds a second way to see the cost: about 23 lines of proof and half a person-day of work for each line of C. Even at the paper's lower estimate for a second kernel, few products can pay that much for 8,700 lines of code.

Why AI Agents Change the Math

Minsky's post gives two reasons for Jane Street's change. One is about cost. The other is about benefit.

Proofs cost less. Minsky writes that agents cannot build hard proofs alone and still need human guidance. But agents know proof tools well, and they do much of the detailed work. In the talk he used the mathematician Terence Tao as an example. Tao is better at math than any model. The model is better at Lean, a language for writing proofs that a computer checks. Together they get more done than either one alone.

Checks matter more. Agents write a lot of code fast. Minsky says agent code "tends towards slop": too complex, with odd bugs, and it breaks the rules of the codebase. People must review all of it, and review is now the bottleneck.

Formal methods help in two ways:

1. They give agents exact feedback. Z3 returns the input that breaks a rule. A proof assistant such as Lean shows which proof step is not complete. The agent uses this feedback to fix its next attempt.
2. They reduce human review. A proof removes the hand check for the rule that it covers. Reviewers then check the spec and the assumptions, not every line.

Minsky also warns that agents "super want to win the video game". If you ask an agent to make all tests pass, it can delete the failing tests. The same risk applies to proofs: an agent can weaken a rule or turn off the check. Keep the spec and the verification job in files that the agent cannot change without human review.

Who Uses Formal Verification Today

Formal verification already runs in production. These examples go from AI output checks to core infrastructure.

AWS Bedrock Guardrails checks LLM output directly. The feature is called Automated Reasoning checks. You upload a policy document, such as a company policy. The system turns it into variables and logic rules. Then it checks each model answer against those rules. Results include VALID, INVALID with a counterexample, and TRANSLATION_AMBIGUOUS. AWS tells users to have a person review the generated rules before use. This is the refund pattern, applied to text answers.

AWS IAM. IAM (Identity and Access Management) decides if a request to an AWS resource is allowed. In an AWS security blog post, Byron Cook says AWS wrote a formal spec of the existing authorization engine, then built a new engine and proved it correct. AWS re-ran the proofs after every change. The new engine is 50% faster than the old one.

AWS Cedar. Cedar is an open-source language for authorization policies. AWS wrote a model of Cedar in Lean and proved its key properties. One proof shows that a matching "forbid" rule always overrides a "permit" rule. The Lean model is 1,673 lines, and the proofs are 5,714 lines. The production code is 24,915 lines of Rust. Every night, AWS runs millions of random inputs through both the Lean model and the Rust code and compares the answers. This is how they keep the model and the real code in step.

Amazon S3 ShardStore. The S3 team used lightweight formal methods on ShardStore, a storage node. They wrote simple reference models as the spec and checked the real code against them. The work stopped 16 issues before production, including crash and concurrency bugs. Engineers who are not formal methods experts now extend the checks.

Vero: AI agents writing verified code. A 2026 benchmark from UC Berkeley and others, Vero, asks agents to write Lean code and proofs for 43 real projects. GPT-5.5 with Codex fully solved 27 projects. Claude Opus 4.8 with Claude Code fully solved 8. Agents passed most single specs but failed on rules shared across a whole project and on long chains of helper proofs.

Mathematics. OpenAI's math repository holds 719 manuscripts from an internal model. About 42% of the top-line results have Lean proofs that a computer checks.

Jane Street. The team is new. In the talk, Minsky said the idea started about eight weeks before the talk, and he called it "a bet". He listed four directions:

The reference approach is the same one that AWS uses for Cedar and ShardStore. People review the simple version. Production runs the fast version. The proof or the comparison tests connect the two.

How to Start

Start with one small function where an error costs money or access. Good first targets in an AI system are:

• Refund, credit, and discount limits.
• Tool permissions: which agent can call which API, for which customer.
• Money and quantity math: balances, fees, inventory.
• Approval rules that you can write as a short list of conditions.

Then follow these steps:

1. Write the rules in plain language. Ask the business owner to approve them.
2. Add rules about what the code must do, not only what it must not do.
3. Move the decision out of the prompt into a small deterministic function.
4. Write the function and its rules in the verification tool.
5. If production runs separate code, check that it matches the model after each change.
6. Run the checks automatically before each code change is accepted. This is continuous integration (CI).
7. Reject the change if a rule fails, the solver returns unknown, or the check does not finish.
8. Keep tests for everything the proof does not cover: model replies, APIs, and the database.

If you cannot state the rule exactly, start with tests and evaluations of model output. Our posts on verifiable outcomes for AI agents and continuous agent verification cover that side.

Put Hard Limits Around Your AI Agents With OpenNash

An AI agent that can move money or change records needs limits that the model cannot change.

OpenNash puts forward-deployed engineers on your team. These are engineers who work inside your company, with your systems and your people. We work with Fortune 2000 companies to take agents from pilot to production:

1. Find the high-risk actions. We list every action that your agents can take, and we rank the actions by the cost of a mistake.
2. Write the rules with your business owners. We turn refund, permission, and approval policies into exact specs that your team signs off.
3. Add checks for those rules. We move each decision into a small function and check it on every change, with a solver or with tests.
4. Test model output on your data. We test each new model version on your own work before you adopt it.
5. Train your team. Your engineers own the specs, the checks, and the CI pipeline when we leave.

Book a call with an OpenNash forward-deployed engineer or email us at hello@opennash.com. In the first session, we review the actions your agents take and pick the limits to check first.