Formal verification is a mathematical proof that a program or system has a given property: for example, that it never goes beyond the bounds of an array or never deletes files outside its working folder. Testing checks a finite number of cases; a proof covers all the cases described by the model. For AI agents, formal checking is applied not to the neural network itself but to its actions: each tool call is checked against a rule by an SMT solver such as Z3.
In brief
- Formal verification proves a property; it does not hunt for bugs on examples.
- An SMT solver checks whether a logical formula is satisfiable with respect to theories: arithmetic, arrays, functions. Z3 is an open-source SMT solver from Microsoft Research under the MIT licence.
- You cannot prove that a model “will not think anything bad”: that runs into Rice’s theorem. You can prove that a specific action does not break a rule: an action has a finite set of parameters.
- Admission is a proof, refusal is a counterexample: the solver either proves that a violation is impossible or finds values under which the rule is broken.
- Time: a decision of the MITR gate under a rule takes 0.95 ms (median, measured on 14 October 2026).
What is formal verification?
It is a set of methods that prove programs correct with the tools of mathematical logic. The property is written as a formula, the program or its model is written as a formula too, and then it is proven that the first follows from the second.
The classic example is the seL4 microkernel. In 2009, a NICTA team (Klein et al., SOSP 2009) proved the functional correctness of its implementation, about 8,700 lines of C, in the Isabelle/HOL proof system; the proof took about 200,000 lines. This level is expensive, so for a long time full verification was used only in critical systems: operating system kernels, avionics, cryptography.
There are lighter forms too: model checking, static analysis that proves individual properties, and checking the satisfiability of formulas with SMT solvers. The last one is the one that fits checking the actions of AI agents.
What are an SMT solver and Z3?
SMT (Satisfiability Modulo Theories) is the problem of whether formulas are satisfiable with respect to theories: integers and reals, arrays, bit vectors, uninterpreted functions. An SMT solver receives a set of assertions and answers:
- sat: the assertions are consistent, and the solver presents example values (a model);
- unsat: the assertions are inconsistent for any values;
- unknown: it could not decide within the resources it was given.
Z3 is an SMT solver from Microsoft Research (de Moura and Bjørner, TACAS 2008), open source on GitHub under the MIT licence; the latest release as of 16 October 2026 is z3-5.3.1 of 15 October 2026. Z3 has bindings for Python, C, C++, Java, .NET and other languages; in Python it is installed as the z3-solver package.
Why is checking an action easier than checking a model’s “thought”?
Rice’s theorem (1953) states that every non-trivial property of the behaviour of programs is algorithmically undecidable. You cannot write a checker that will tell, for any program, whether it will ever do something bad. A language model with its planning is in effect such a program, and “proving that the agent will never want to delete the database” is impossible in the general case.
But a tool call is not behaviour; it is one specific object: the tool’s name, a path, an amount, a recipient. Checking whether it satisfies a rule is a problem of a different class. If the rule is written in a decidable fragment of logic, for example quantifier-free, with linear integer arithmetic and uninterpreted functions (QF_UFLIA), the solver is guaranteed to give an answer.
Hence the principle: do not try to verify the model; verify each of its actions at the boundary with the outside world.
What does “admission is a proof, refusal is a counterexample” mean?
The rule is written as a safety condition, and the facts as the parameters of the call. The solver receives the negation of the condition together with the facts:
- unsat: the condition cannot be violated with these facts. This is a proof of admissibility, and the action is admitted;
- sat: there are values under which the condition is violated. This is a counterexample: it shows exactly what is wrong and suggests how to fix the action.
A simple Python example: an agent is allowed payments no larger than a limit.
from z3 import Int, Solver, Not
amount, limit = Int('amount'), Int('limit')
s = Solver()
s.add(limit == 100000) # rule: the payment limit
s.add(amount == 120000) # fact: the amount in the agent's call
s.add(Not(amount <= limit)) # negation of the safety condition
print(s.check()) # sat: there is a violation, the call is refusedFor an amount of 90,000 the same code prints unsat: a violation is impossible, and the call is admitted. If the call lacks a fact the rule needs, admissibility is not proven, and that is a refusal too.
How does this work in the MITR gate?
In the institute’s MITR gate, admission rules are data files (YAML); as of 14 October 2026 they are defined for 19 classes of actions, and the solver’s logic is QF_UFLIA. Admission is a proof (unsat), refusal is a counterexample with the conditions for a fix, and if a class of actions has no rule, the solver refuses. A language model takes no part in the decision. The refusal is enforced in enforce mode; as of 14 October 2026 this mode is switched on for file deletion, and the other classes run in advisory mode.
How such a check differs from text filters is explained on the page about guardrails; the earlier architecture of the gate is described on the page MITR: architecture and rationale (in Russian).
How much time does a check take?
As of 14 October 2026, a decision of the MITR gate under a rule takes 0.95 ms (median), and a call together with an explanation takes 4.26 ms; earlier measurements were 0.74 and 3.31 ms (26 September 2026, 17 rules) and 0.87 and 4.43 ms (2 October 2026). For comparison, a network call to an external service usually takes tens of milliseconds, so the check does not become a bottleneck.
The time depends on the complexity of the rule and the logic. In decidable quantifier-free fragments the solver answers quickly, while rules with quantifiers or non-linear arithmetic may take far longer or return “unknown”. That is why rules for actions are written in a simple fragment.
Frequently asked questions
What is formal verification in simple terms?
It is a mathematical proof that a program has the required property for all possible inputs, not only on the examples that were checked. For example, a proof that a function will never write data beyond the bounds of a buffer.
How does formal verification differ from testing?
A test checks a finite number of cases and may miss a bug in a case that was not checked. Formal verification proves the property for all the cases described by the model, but it requires a precise statement of the property and of the model.
What is Z3?
An open-source SMT solver from Microsoft Research under the MIT licence. It checks the satisfiability of logical formulas with respect to arithmetic, arrays, functions and other theories; it is available from Python (the z3-solver package), C, C++, Java and .NET.
Can the safety of a neural network be formally proven?
Not completely: by Rice’s theorem, non-trivial properties of the behaviour of programs are undecidable, and neural networks are probabilistic as well. Individual properties of small networks are proven with special methods, but in practice, for agents, it is not the model that is checked but each of its actions against a rule.
What does “admission is a proof, refusal is a counterexample” mean?
The solver receives the negation of the rule together with the parameters of the action. If the formula is unsatisfiable (unsat), a violation is impossible, and the action is admitted. If it is satisfiable (sat), the solver presents a counterexample, the values under which the rule is violated, and the action is refused.
Sources
- Z3 Theorem Prover, GitHub (release z3-5.3.1 of 15 October 2026, MIT licence): https://github.com/Z3Prover/z3
- L. de Moura, N. Bjørner, “Z3: An Efficient SMT Solver”, TACAS 2008
- G. Klein et al., “seL4: Formal Verification of an OS Kernel”, SOSP 2009
- H. G. Rice, “Classes of Recursively Enumerable Sets and Their Decision Problems”, Transactions of the AMS, 1953
- ANO Scientific Research Institute of System Synthesis: measurements of the MITR gate of 26 September, 2 October and 14 October 2026
Checked: 16 October 2026