← Back to Blog

The Verification Bottleneck

AI agents generate code much faster than humans can verify it.

Can an AI generated implementation be verified automatically?

Engineers already give AI agents specifications: prompts, tickets, acceptance criteria, API contracts.

Usually those specifications are informal and ambiguous.

A formal specification makes intent precise enough to verify automatically.

A Door

Consider a door: it can be open or closed.

If it is closed, it can be opened. And if it is open, it can be closed.

closed --opened--> open
open   --closed--> closed

This behavior is the specification.

Implementation

Now consider an implementation with extra steps:

closed --τ--> opening --opened--> open
open   --τ--> closing --closed--> closed

The door can be opening and closing.

But the specification only sees open and closed.

We want to verify that the extra states and extra steps preserve the specification.

Labeled Transition Systems

The door behavior can be modeled as a Labeled Transition System(LTS): a graph whose nodes are states and whose edges are labeled transitions.

structure LTS (State : Type u) (Label : Type v) where
  Tr : State → Label → State → Prop

The specification has two states: closed and open.

inductive SpecState where
  | closed
  | open
deriving DecidableEq, Fintype

The implementation has four states: closed, opening, open, and closing.

inductive ImplState where
  | closed
  | opening
  | open
  | closing
deriving DecidableEq, Fintype

Both systems use the same visible transitions: opened and closed.

inductive Label where
  | opened
  | closed
  | τ
deriving DecidableEq, Fintype

The implementation also uses τ, a silent internal transition.

The specification and implementation LTSs are constructed this way:

def spec : LTS SpecState Label :=
  LTS.mk fun
    | .closed, .opened, .open => True
    | .open, .closed, .closed => True
    | _, _, _ => False

def impl : LTS ImplState Label :=
  LTS.mk fun
    | .closed, .τ, .opening => True
    | .opening, .opened, .open => True
    | .open, .τ, .closing => True
    | .closing, .closed, .closed => True
    | _, _, _ => False

Verify

To prove that the implementation preserves the specification, we relate states from both LTSs.

A related pair means: these two states have the same visible behavior.

The relation must be stable.

If one side performs a visible transition, the other side must be able to perform the same visible transition, possibly with silent τ transitions before or after it.

After the transition, the resulting states must be related again.

For the door:

implementation: closed --τ--> opening --opened--> open
specification:  closed ----------------opened--> open

and:

implementation: open --τ--> closing --closed--> closed
specification:  open ----------------closed--> closed

So the extra states are allowed because they do not change the visible behavior.

In Lean:

example : LTS.WeakBisimilarity impl.toLTS spec.toLTS .closed .closed :=
  weakBisimilar?_sound impl spec (s₁ := .closed) (s₂ := .closed) (by decide)

You can look at all the code.

Conclusion

Note that this is a proof, not a test.

Tests provide confidence by exploring executions of a program.

Tests are a great tool, particularly property-based and fuzzing tests.

But a proof checks all executions covered by the model.

Formal verification guarantees that the proven properties are correct.

And automatically doing this is very powerful to leverage AI agents code generation.

Sources