Formal verification is using math to prove that a system cannot break certain rules. In other words, to formally verify a system means to mathematically prove that it behaves as expected and cannot do certain things we do not want it to do. Today, formal verification is most often used in places where failure is very expensive or dangerous, such as hardware and semiconductor verification, cryptography and security-critical infrastructure, and high-assurance systems like aerospace and kernels.

In this post, I explain how formal verification works and use the example of an authorization system to show how it can raise security guarantees.

Formal verification turns a system into a mathematical model and then proves statements about this model. The kind of math usually involves logic, set theory, graph and state-machine reasoning, algebra and symbolic reasoning, theorem proving, constraint solving, SAT, and SMT solving. 

Let’s use a simple agent authorization system as an example.

We have a system. The system has a state. The system state includes: 

• The agent and its permissions

• The database and its operations: read, write, delete

• The policy which says that delete is forbidden

Our toy system is: We have an agent called SupportAgent. It works with a database called CustomerDB. The database supports three operations: read, write, and delete. The policy says that SupportAgent is allowed to read and write, but it is never allowed to delete.

A state transition happens whenever the agent requests an operation and the system evaluates it. If SupportAgent requests read on CustomerDB, and the policy allows it, the system moves into a new state where the read has happened. If SupportAgent requests delete on CustomerDB, the system should move into a new state where the request is denied and the database remains unchanged.

Now we define the property we care about. In our example, the property is: SupportAgent must never be able to delete CustomerDB. That is the security guarantee we want from the system.

This is the point where formal verification starts. 

We ask: is there any possible sequence of valid state transitions that could lead to a forbidden state? In this case, the forbidden state is a state in which SupportAgent has successfully deleted CustomerDB.

This check is performed by Solver, which either finds a sequence of valid steps that leads to the forbidden state, or if it cannot find any such path, then the property is proven within the model.

For our toy example, solver engages logic, set theory, state-machine reasoning, graph reasoning, and symbolic reasoning.

Set theory

Set theory is used to define the objects in the system and how they relate. 

In our example:

• Agents = {SupportAgent}

• Resources = {CustomerDB}

• Operations = {read, write, delete}

• AllowedOperations (SupportAgent, CustomerDB) = {read, write}

• delete is not in AllowedOperations(SupportAgent, CustomerDB)

State-machine reasoning 

A state is a snapshot of the system at one moment.

So state-machine reasoning is the part that says:

• what a state is

• what the next possible states are

• which transitions are legal

For example, the state might be:

• agent = SupportAgent

• target = CustomerDB

• request = none

• database deleted = false

Possible moves are:

• from “no request” to “read requested”

• from “read requested” to “read succeeded”

• from “delete requested” to “delete denied”

Graph reasoning

Once we have states and transitions, we can view the whole system as a graph.

In that graph: each node is a state and each edge is a valid transition. 

Graph representation of states and state transitions allows checking for reachability of undesired states. Is the bad node reachable from the initial node? If the answer is yes, there is a path to failure.

Symbolic reasoning

Symbolic reasoning is what allows the solver to reason over many possible executions at once, through variables and constraints, rather than enumerating each case. It helps to reason about all agents in the system or all delete actions in the system at once.  

We declare:

a = any agent

d = any database

op = any operation

s = any state

Then a symbolic formula for the policy is: For every agent a and every database d, if delete is not allowed for a on d, then a can never successfully delete d.

Written more formally:

for all a, d, s:
if Reachable(s)
and NotAllowed(a, delete, d)
then not Success(s, a, delete, d)

Logic

Solver turns the system and the policy into a set of logical statements:

1. For every state s and next state s':
   if Request(s, SupportAgent, Read, CustomerDB)
   and Allowed(SupportAgent, Read, CustomerDB)
   then Success(s', SupportAgent, Read, CustomerDB)

2. For every state s and next state s':
   if Request(s, SupportAgent, Write, CustomerDB)
   and Allowed(SupportAgent, Write, CustomerDB)
   then Success(s', SupportAgent, Write, CustomerDB)

3. For every state s and next state s':
   if Request(s, SupportAgent, Delete, CustomerDB)
   and Not Allowed(SupportAgent, Delete, CustomerDB)
   then Denied(s', SupportAgent, Delete, CustomerDB)
   and Unchanged(s', CustomerDB)

The outcome we want to prevent (agent deleting) is stated as following: Success(s, SupportAgent, Delete, CustomerDB).

Constraint solving

Once the system and the policy have been written as logical statements, the solver takes the bad outcome we want to prevent and tries to make it true together with all the other rules using constraint solving.

Variables:

RequestRead, RequestWrite, RequestDelete

AllowRead, AllowWrite, AllowDelete

SuccessRead, SuccessWrite, SuccessDelete

DeniedDelete

DatabaseDelete

Constraints:

AllowRead = true

AllowWrite = true

AllowDelete = false

exactly one of RequestRead, RequestWrite, RequestDelete is true

SuccessRead if and only if RequestRead and AllowRead

SuccessWrite if and only if RequestWrite and AllowWrite

SuccessDelete if and only if RequestDelete and AllowDelete

DeniedDelete if and only if RequestDelete and not AllowDelete

DatabaseDeleted if and only if SuccessDelete

Forbidden outcome:

DatabaseDeleted = true

A solver keeps propagating consequences like this:

• if DatabaseDeleted is true, then SuccessDelete must be true

• if SuccessDelete is true, then RequestDelete and AllowDelete must be true

• but AllowDelete is already fixed to false

• contradiction reached

This process is called constraint propagation. The solver keeps deriving consequences from the rules until one of two things happens: it finds a contradiction or it finds a full assignment that satisfies everything.

Theorem proving

As a theorem, the undesired property is: in every reachable state, SupportAgent has not deleted CustomerDB. 

Then it proves it in two steps: 

1. Base case: Is it true for the initial state?

2. Induction: Assume the property is true in some state s. Then prove it is still true after any allowed transition from s to s'.

So it checks all possible transition types:

• if SupportAgent requests read, the database is still not deleted

• if SupportAgent requests write, the database is still not deleted

• if SupportAgent requests delete, the policy denies it, so the database is still not deleted

If all transitions preserve the property, then the theorem prover concludes: the property holds in all reachable states

As you could see above, formal verification is a combination of various mathematical tools to reason about the whole system all at once and not particular cases. We have listed just some of them, in real systems, solvers use even more tools.

When we turn a company environment and its policy into a mathematical model, we can reason about the properties we want to hold. When we think about getting from point A to point B in an existing system, there can be multiple ways to get there. Some of them are more obvious, such as calling the endpoint directly, while others are less obvious and may consist of several steps.

Automated reasoning applies logic and mathematical inference to determine all possible access paths allowed by a policy, not just the obvious ones. Instead of asking only whether an agent can directly perform a forbidden action from the current state, the system asks whether there exists any reachable state in which that action becomes possible.

This is especially important for agentic systems because of the nature of agents as actors. They are not humans acting in good faith, and they are not hackers acting with malicious intent. Most of the time, they are doing legitimate things, but sometimes a chain of legitimate actions can still produce a harmful outcome. Unlike humans, they act non-deterministically, operate at machine speed, and are constantly looking for broader context and more ways to complete a task. If there is a path in the system to a forbidden outcome, the probability that a human will discover it by accident is almost zero, while an agent will eventually discover it.

Formal verification also meaningfully reduces false positives because it derives from the actual policy logic and all possible access paths, rather than predicting risk from heuristics. This matters because heuristic systems are more likely to overfire with agents, since there are many more actions and combinations of actions that may look suspicious on the surface.

_______________________________________________________________________

Acknowledgment: I learned a lot from studying Amazon’s work on formal verification in authorization systems, and from many thoughtful discussions that helped sharpen my understanding.

Thank you for reading. You are welcome to reach out with questions, ideas, and suggestions: lisaakselrod@gmail.com