TLA+ was developed by Leslie Lamport in the 1990s as a formal specification language for describing and verifying distributed systems. Amazon Web Services has used it to verify the correctness of critical systems including DynamoDB, S3, and EBS. Microsoft uses it for Azure. It is a mature, well-understood tool with a track record in production environments where failures are expensive.
The question we set out to answer was whether the same approach could be applied to AI agent safety. Not as a research exercise, but as a production engineering practice.
Why testing is not sufficient
Testing finds problems that your tests cover. Adversarial inputs are designed specifically to avoid what you have covered. A test suite that passes completely tells you the system behaves correctly on the inputs you thought to test. It does not tell you the system is correct.
This is a known limitation in safety-critical engineering. Avionics, medical devices, and nuclear control systems are not validated by testing alone. They are formally specified and verified. The property you care about is stated precisely, and a tool exhaustively checks whether the system satisfies that property across all reachable states.
AI agent systems are not yet treated this way. They should be, and eventually will be required to be, in any regulated context where agents take consequential actions.
What we verified and how
We specified the Dynamic Broker Architecture as a TLA+ model and defined 21 safety invariants: properties that must hold in every reachable state of the system. These include constraints such as an agent with read-only permissions cannot execute write operations, a revoked token cannot be used to authorize any action, and no action can be executed without a corresponding policy record.
The TLC model checker explored 183 billion reachable states of the system and found zero invariant violations. This is not a claim that the implementation is bug-free. It is a claim that the design, as specified, satisfies the stated safety properties under all conditions the model can represent.
Zero violations across 183 billion states means the safety properties hold by construction in the architecture, not by the absence of tests that would have found a problem.
The engineering challenge
The hard part of formal verification is not running the model checker. It is correctly specifying what you want to verify. A specification that does not capture the real system tells you nothing useful. A property that is specified too loosely can be satisfied trivially.
Getting the specification right requires deep understanding of the system's threat model. Each invariant we verified corresponds to a real attack vector: token replay, privilege escalation, policy bypass, action spoofing. The verification is only as useful as the quality of the invariants it checks.
This is also why formal verification is not a one-time exercise. As the system evolves, the specification must be updated and re-verified. That is a maintenance commitment, not a checkbox.
What this means for enterprise deployments
Organizations deploying AI agents in enterprise environments will increasingly face questions about how safety properties are verified. Regulators, auditors, and enterprise security teams will ask how you know the agent cannot take actions outside its defined scope.
The honest answer for most AI systems today is that testing has been performed against known attack patterns. That answer is not sufficient for consequential deployments. The standard that will emerge, and that is already emerging in regulated industries, is formal verification of the safety-critical components of the system.
We built to that standard from the beginning. Not because it was required, but because it is the only answer to the verification question that holds up under scrutiny.
Formally verified AI security infrastructure
The Dynamic Broker Architecture provides infrastructure-layer AI security with formal verification of its core safety properties.
Learn about DBA