Testing samples the input space. Formal verification covers it. The distinction is Dijkstra famous line that testing shows the presence of bugs but never their absence, and formal methods are the response: express the property you care about as a mathematical statement, then prove it holds for all inputs, or produce a concrete counterexample. The main families are model checking, which exhaustively explores a finite state space; theorem proving, which constructs a machine-checked proof in a system like Coq, Isabelle, or Lean; abstract interpretation, which soundly over-approximates program behavior; and SMT solving, which sits underneath most of the practical tooling.
This is not an academic curiosity. The seL4 microkernel has a machine-checked proof of functional correctness. CompCert is a C compiler proven not to introduce bugs during optimization. AWS uses automated reasoning on IAM policies in Zelkova and on TLS implementations in s2n. Intel formally verifies floating point units, a habit acquired expensively after the Pentium FDIV recall. Avionics under DO-178C and rail signalling under EN 50128 both accept formal methods in place of some testing. Where correctness is worth more than velocity, this is normal engineering.
Then you point it at a language model and it stops working, and it is worth being honest about why. Two reasons, and neither is a tooling gap. First, there is no specification. Formal verification proves conformance to a precise statement, and helpful, harmless, and honest are not precise statements; nobody can write them down in logic, which means there is nothing to prove. Second, even for properties that can be stated, the scale defeats it. Neural network verification tools like Reluplex and Marabou can prove local robustness properties on networks with thousands of neurons. Frontier models have hundreds of billions of parameters and take unbounded natural language as input. The gap is many orders of magnitude and is not closing soon.
The useful move is to stop trying to verify the model and start verifying the harness around it. The model is a probabilistic component; everything else in an agent is ordinary software with ordinary semantics. Permission checks, spending caps, output schemas, workflow state machines, rate limits, tenant isolation, and sandbox boundaries can all be specified and, for the ones that matter most, formally checked. This gives you the architecture that actually holds up under adversarial pressure: an unverified model contained inside a verified boundary, where the model can propose anything and the boundary decides what is permitted. Any safety property you enforce by asking the model nicely in a system prompt is a property you have not enforced.
The other direction is more interesting than it first sounds, which is using models to produce formal artifacts. Generating Lean or Coq proofs, or code with proof obligations a checker discharges, converts the hallucination problem into something a machine can adjudicate. The model proposes and the checker disposes, and a proposal that fails the check costs nothing. That pairing is one of the few places where a probabilistic generator and a guarantee coexist cleanly.
Why It Matters
As agents get permissions to spend money, modify records, and call external systems, the question of what a system cannot do stops being philosophical and starts being an audit finding. We tested it thoroughly does not answer a regulator asking whether an outcome is possible. Formal methods on the constraint layer let you make a small number of load-bearing guarantees that no prompt, no jailbreak, and no injected instruction can invalidate, which is a fundamentally different assurance than any amount of red teaming can give you.
Example
An agent can issue customer refunds. The first design puts the rule in the system prompt: never refund more than 500 dollars, and never more than 2,000 dollars per account per day. It survives casual testing and fails the first time a customer pastes a crafted support ticket containing instructions the model treats as its own. The second design moves the rule behind a policy engine with a checked invariant over the transaction log, so no sequence of tool calls can exceed the cap regardless of what the model requests. Injection can still make the model try. It can no longer make the cap fail.