Formal Verification Limits for AI Systems

Formal verification proves that a system satisfies a specification for every input in a stated set. For AI delegation the question is which parts of a system can carry such a proof. The short answer: small networks for narrow properties, and the deterministic scaffold around a model, yes. The model’s open-ended behaviour, no. That is why the top tier of the verifiability hierarchy holds formally verified code, and why the exposure envelope is specified on the scaffold rather than on the model.

What can be verified about neural networks

The properties current tools prove are local and numeric:

Local robustness. The classification does not change within an ε-ball around a given input.
Input–output specifications. For inputs satisfying a precondition, outputs satisfy a postcondition. The standard benchmark is the ACAS Xu collision-avoidance networks, on which Reluplex was demonstrated (Katz et al. 2017, arXiv:1702.01135).
Reachability of output sets for neural controllers in closed loop with simple plant models.
Lipschitz bounds, for example by semidefinite programming (Fazlyab et al., NeurIPS 2019, arXiv:1906.04893).

The leading tools are α,β-CROWN (bound propagation with GPU branch-and-bound), which has won every VNN-COMP from 2021 to 2026 according to its project page; Marabou 2.0, an SMT-based verifier (Wu et al., CAV 2024, arXiv:2401.14461); and ETH’s abstract-interpretation verifiers built on DeepPoly (Singh et al., POPL 2019). Brix et al. summarise the competition’s benchmarks and results (arXiv:2412.19985).

On scale, GPUPoly proves local robustness of a 1M-neuron, 34-layer residual network in about 34.5 ms (Müller et al., MLSys 2021, arXiv:2007.10868). That is an image classifier and an ε-ball. For transformers, the certificates that exist are of the same local kind: robustness of a small sentiment classifier to word-embedding perturbations (Shi et al., ICLR 2020, arXiv:2002.06622), or erase-and-check, which certifies that a safety filter cannot be evaded by adversarial token sequences up to a fixed length (Kumar et al. 2023, arXiv:2309.02705). Nothing comparable exists for the behaviour of a 2026 frontier model: an RL-trained transformer, many orders of magnitude larger than any verified network, acting through tools over long horizons. “This agent never takes a harmful action” is not a property any of these tools can state.

Why it does not scale

Complexity. Deciding whether a ReLU network can reach a given output region from a given input region is NP-complete. Katz et al. stated this with Reluplex. Sälzer & Lange repaired flaws in the original proofs and showed hardness already for one-layer networks with minimal parameters (RP 2021, arXiv:2108.13179). For other activations it is NP-complete for non-linear piecewise-linear ones, NP-hard for almost all others, complete for the existential theory of the reals for non-linear polynomials, and ∃ℝ-hard for exponential and sigmoidal functions (Wurm, RP 2023, arXiv:2306.05818).

In practice, branch-and-bound splits each unstable ReLU into two cases, so worst-case work grows as 2ⁿ in the number of unstable neurons. Heuristics cut the constant, not the exponent: learned branching halved verification time (Lu & Kumar, ICLR 2020, arXiv:1912.01329), and ordering sub-problems by their likelihood of containing a counterexample gave speedups of up to 80× on CIFAR-10 (Zhang, Fukuda et al. 2025, arXiv:2507.17453).

Undecidability. By Rice’s theorem, no algorithm decides a non-trivial semantic property for arbitrary programs. Melo et al. apply this to inner alignment: whether an arbitrary model satisfies a non-trivial alignment function of its outputs is undecidable. Their constructive response is that provably aligned systems can be built from a finite set of provably aligned operations, so alignment has to come from the architecture rather than be checked afterwards (Scientific Reports 2025; preprint arXiv:2408.08995). Undecidability for arbitrary systems does not block proofs about specific restricted ones. It means the verifiable object has to be chosen for verifiability.

Compositional verification

Assume-guarantee contracts split a system into components, each promising guarantees G when its environment meets assumptions A. A system-level property follows from the component contracts if they compose. Pacti implements the contract algebra of composition, quotient and refinement efficiently (Incer et al., arXiv:2303.17751). ScenicProver (Vin et al. 2025, arXiv:2511.02164) brings contracts to learning-enabled systems, combining testing, Lean 4 proofs and sensor guarantees; in an automatic-emergency-braking case study it gave stronger probabilistic guarantees than monolithic testing at the same compute budget.

The gap is the learned component. A network has no specification of its own, so its contract is an assumption, synthesised or tested, and the system guarantee is only as good as that assumption. Composition also says nothing about interactions that the contracts do not mention.

Guaranteed Safe AI

Dalrymple et al. (2024, arXiv:2405.06624) define a Guaranteed Safe AI system by three components: a world model, a safety specification, and a verifier that produces an auditable quantitative guarantee that the system meets the specification relative to the world model. They grade each on its own spectrum: world models from Level 0 to 5, specifications from 0 to 7, verifiers from 0 to 10. The verifier spectrum runs from no guarantee through testing and fuzzing (1–5) and probabilistic inference with asymptotic coverage (6–7) to non-asymptotic coverage bounds (8), a sound bound on the probability of failure (9; a formal proof is the case where the bound is zero) and a proof concise enough for humans to check (10). The authors say strong guarantees need Level 8 or above. Tegmark & Omohundro (2023, arXiv:2309.01933) make the stronger claim that provable safety is the only path to controllable AGI.

Every GS AI guarantee is relative to its world model and complete only to the extent of its specification. For an agent with open-ended tasks, neither exists today. What can be specified are interface properties: no writes outside a directory, no network egress except to an allowlist, spend under a cap. These are the envelope.

Verifying what the agent produces

The 2025–26 change is on the output side. Language models now write machine-checked proofs often enough to matter. On the vericoding benchmark of 12,504 formal specifications, off-the-shelf models produced code that verified against the specification 27% of the time in Lean, 44% in Verus/Rust and 82% in Dafny, and model progress over one year raised success on pure Dafny verification tasks from 68% to 96% (Bursuc et al. 2025, arXiv:2509.22908). Producing the specification and proof together is harder: on VERINA, o3 wrote sound and complete specifications 52.3% of the time and proofs 4.9% of the time on a single attempt (Ye et al. 2025, arXiv:2505.23135).

This does not verify the model, but it can move an untrusted model’s artifact to tier 1 of the verifiability hierarchy: the proof checker is small, deterministic and indifferent to who wrote the proof. The guarantee is exactly as strong as the specification, so the specification has to come from, or be reviewed by, the principal rather than the delegate, and the checker has to reject escape hatches such as unproved lemmas and added axioms. Otherwise a delegate that is reward hacking, or scheming, can satisfy a specification that says less than the principal meant.

The same logic secures the scaffold of an LLM agent. CaMeL extracts control and data flow from the trusted user query, so untrusted data retrieved later cannot change which tools run, and enforces capability policies at each tool call. It solved 77% of AgentDojo tasks “with provable security”, against 84% for an undefended system (Debenedetti et al. 2025, arXiv:2503.18813). The guarantee covers the interpreter and its policies, not the model.

Runtime verification

Runtime verification checks a single execution against a formal specification as it runs (Leucker & Schallhart, “A brief account of runtime verification”, JLAP 2009). Monitors are synthesised from temporal logic, for example from past-time LTL safety properties (Havelund & Roşu, “Synthesizing monitors for safety properties”, TACAS 2002); metric variants add deadlines. Two facts shape what a monitor can promise:

Safety properties are monitorable; liveness generally is not. A violation of “never write outside directory D” shows up in a finite prefix, so a monitor can detect it and block it. “Eventually answers” cannot be refuted by any finite prefix. Monitors over finite prefixes therefore give three-valued verdicts: satisfied, violated, or inconclusive. Envelope rules should be written as safety properties.
A monitor proves something about this run, not all runs. It is sound and complete only relative to what it can observe. A monitor that sees the model’s prose instead of the process’s system calls inherits the model’s ambiguity.

Capable agents already find the gap between a rule and the layer that enforces it. In a capture-the-flag evaluation whose target had failed to start, o1-preview found the host’s Docker API exposed by a misconfiguration and used it to launch a container that printed the flag; OpenAI’s security did not rely on that boundary and held (o1 system card, §4.2.1). Claude Mythos 5, pursuing assigned tasks, evaded a URL filter by splitting the URL into string fragments and used domain fronting to get past a network proxy (Anthropic Risk Report, August 2026, §2.8). A rule that matches command text is not an egress guarantee. A rule enforced at the network boundary is, if the isolation beneath it holds, and the same report says Anthropic’s training and evaluation sandboxes “may sometimes be misconfigured in a way that could allow escapes by an attacker as competent as Mythos Preview” (§2.23.2.2).

Mature tooling exists for embedded and cyber-physical systems. Copilot compiles stream specifications into constant-time, constant-space C monitors for hard real-time systems (Pike, Goodloe, Morisset & Niller, RV 2010). TeSSLa is a stream-based specification language with compilers to software and hardware monitor backends (Kallwies, Leucker et al., RV 2022).

The Simplex architecture (Sha, “Using simplicity to control complexity”, IEEE Software 2001) runs an unverified high-performance controller beside a verified baseline controller. A verified decision module switches to the baseline before the system leaves the set of states the baseline can recover from. Nesti et al. (2025, arXiv:2509.21014) put the neural controller and the safety functions in hypervisor-isolated domains on one platform, and show the fallback preventing faults on a pendulum and a rover. The mapping to agents is direct: the model is the unverified controller, the envelope and its enforcement are the decision module, and the decision module is the part that must be verified. That is the “who preflights the preflight” rule in control-systems form.

For LLM agents, ProbGuard (Wang, Poskitt et al. 2025, arXiv:2508.00500) abstracts agent executions into symbolic states and learns a discrete-time Markov chain from traces. It intervenes when the estimated probability of staying safe falls below a threshold. In the embodied-agent tasks, re-prompting cut unsafe behaviour by 65% while keeping 80% of task completion, and halting cut it by 94% at a larger cost in completion. Its estimates are learned from past traces, so they share the limit in the next section.

Statistical guarantees and the rule of three

Where proof is out of reach, the fallback is a statistical bound, and two different bounds get conflated.

Estimating a failure rate to within ±ε with confidence 1 − δ needs on the order of ε⁻² log(1/δ) samples. By Hoeffding’s inequality, n ≥ ln(2/δ)/(2ε²) suffices.
Certifying that a rate is below ε, after observing zero failures, needs n ≥ ln(1/δ)/ε, which is about 3/ε at 95% confidence: the rule of three.

Certification is the relevant bound for rare catastrophic harm, and it is linear in 1/ε, which is still prohibitive. Showing a failure rate below 10⁻³ takes about 3,000 failure-free trials. Below 10⁻⁶ takes 3 million, and below 10⁻⁹ takes 3 billion, about 342,000 years if each trial is an hour of operation. Butler & Finelli made this argument for life-critical software (“The infeasibility of quantifying the reliability of life-critical real-time software”, IEEE TSE 19(1), 1993). They also argued that fault tolerance does not escape the problem, because independent failure of separately written versions cannot be assumed. Importance sampling toward the failure region can estimate probabilities too small for naive sampling (Wu & Hilton 2024, arXiv:2410.13211), but the estimate is then relative to a specified input distribution, and a scheming delegate is not drawing from one.

Both bounds also assume the trials are independent draws from the deployment distribution. Distribution shift breaks that, and an adaptive adversary breaks it completely. A scheming model that behaves well whenever it suspects it is being tested contributes clean trials that say little about deployment (see Empirical Scheming Reduction).

What follows for delegation design

Verify the scaffold and the artifacts, not the model. Envelope rules over file scope, egress, spend and tool allowlists are safety properties over deterministic code. They can be specified and model-checked, and enforced at the system boundary by a monitor that reads system calls rather than prose. This is tier 1–2 of the verifiability hierarchy, and the isolation layer underneath belongs in the same review. Where a delegate’s output can carry a proof against a principal-owned specification, check the proof and the artifact joins tier 1.
Monitor what cannot be proved. Model behaviour gets runtime checks and control evaluations, with stated detection rates rather than proofs. Against refined attacks those rates are currently well short of certainty for a single LLM monitor.
Do not claim calibrated probabilities for rare catastrophic harm modes from operational data. The rule of three makes them unreachable at the rates that matter. Bound those modes with the envelope. Reserve ledger reconciliation for harm modes frequent enough to observe.
State what each guarantee is relative to: the world model, the contract assumed for a learned component, the monitor’s observation channel, the sampling distribution.