Formal Verification Is Becoming Mandatory

You are about to get pwned by agents that are better at hacking and reading code than your agents are at writing code. In the Agentic Era, Formal Verification is mandatory.

Unless your binary is formally correct, models will find 0-days in your code, the compiler you used, or a 3rd party library.

Very few people know about Formal Verification techniques, but they are about to become very important because the models are getting so good at breaking into "secure" systems.

In ordinary programming, we write code and a bunch of tests and hope that we covered all the important cases, but with formal verification, we write a mathematical contract using a tool like Dafny (with an SMT solver like Z3) to mathematically prove that the code always obeys that contract, so no more "it works on my machine."

So let's say we wanted to find the biggest number in an array of numbers (or integers) – how would we do it?

We can write a method FindMax that loops over the elements of an array a comparing each element a[i] to the biggest known max value and if it's bigger than max, we update max. By the time we get to the end of the array, the newest max value is the biggest, or maximum.

Here is how that looks in Dafny, where // means my comments:

method FindMax(a: array<int>) returns (max: int) // takes an array of integers `a` and returns an integer, `max`
{
  max := a[0]; // assume the first element a[0] is biggest
  var i := 1; // an iterator `i` = 1 to loop over rest of the array
  while i < a.Length // loop over the length of the array
  {
    if a[i] > max { // if current element a[i] is bigger than max,
      max := a[i]; // then update max.
    }
    i := i - 1; // increment i for the next loop iteration
  }
}

Is it correct? Does it terminate? Who knows – there could be a bug where it loops forever, or reads beyond the array. What happens if we pass in an empty array?

Actually, it is totally wrong: it will fail because a[0] reads beyond the length of the empty array. i := i - 1 decrements i so it will read backwards into the array – you probably didn't notice that.

So what we can do here is add a mathematical contract with various pre- & post-conditions and invariants that must hold during execution:

method FindMax(a: array<int>) returns (max: int)
  requires a.Length > 0 // precondition
  ensures  forall i :: 0 <= i < a.Length ==> a[i] <= max // postcondition (everyone ≤ max)
  ensures  exists i :: 0 <= i < a.Length && a[i] == max // postcondition (max actually appears)
{
  max := a[0];
  var i := 1;
  while i < a.Length
    invariant 1 <= i <= a.Length // i must not exceed length of array
    invariant forall j :: 0 <= j < i ==> a[j] <= max // all prior elements should be equal or less than max
    invariant exists j :: 0 <= j < i && a[j] == max // there exists an element in the array, a[j] that matches the current max value
    decreases a.Length - i // proves the loop terminates
  {
    if a[i] > max {
      max := a[i];
    }
    i := i + 1;
  }
}

What does this even mean? In order:

1. The array must not be empty (otherwise what number do we return?)
2. max must not exceed any number in the array
3. max must match one of the numbers in the array

And inside the while-loop:

1. We must not read beyond the array, i.e. i must be less than the length of the array, a.Length
2. All previously seen elements should be less than or equal to max
3. The max number must exist somewhere in the array
4. On each loop, increase i so that (a.Length - i) decreases, ensuring that the loop eventually terminates

This then goes through these compilation steps:

1. Dafny source
    ↓  (parser + type checker + resolver)
2. Boogie intermediate language
    ↓  (verification-condition generator)
3. SMT formulas (first-order logic with arrays, quantifiers, arithmetic…)
    ↓
4. Z3 (or another SMT solver)

The Dafny code gets turned into Hoare logic which is encoded in Boogie, e.g.

a.Length > 0
∧ max := a[0]
∧ i := 1
⇒
  1 ≤ i ≤ a.Length
∧ (∀ j • 0 ≤ j < i ⇒ a[j] ≤ max)
∧ (∃ j • 0 ≤ j < i ∧ a[j] == max)

This Hoare Logic is then encoded to SMT logic for Z3, e.g.:

(assert
  (forall ((i Int))
    (=> (and (<= 0 i) (<= i n) (< i n))   ; Inv ∧ Guard
        (and (<= 0 (+ i 1))               ; after i := i+1
             (<= (+ i 1) n)))))

Z3 reduces the problem to a system of linear inequalities and uses a highly engineered Simplex + cutting-plane procedure to prove the system has no counter-example without actually enumerating every possible array of numbers (which would take forever).

Z3 will output a counter-example that violates the invariants, sat for satisfied, or "unknown" if it can't prove the invariant.

Z3 also uses big words like,

• quantifier instantiation,
• the theory of arrays,
• linear arithmetic,
• and congruence closure (whatever that means)

These kinds of techniques can also be used for performance optimization to check that your program isn't doing something expensive, but the main focus is correctness.

Formal Verification of EACL

EACL is my open-source situated ReBAC authorization library. You can play with it on the EACL Explorer, backed by in-memory DataScript.

Authorization libraries have to be first-and-foremost correct. Secondly they must be fast.

So for the last 1 day & 9 hours, I have been doing agentic formal verification to ensure that EACL is correct, and to search for performance issues.

Already multiple weird bugs and performance issues have been found and fixed (usually related to cursor or cache), which is why the speed of the latest version of EACL v8.0 is absolutely stellar, partly owing to the new sub-graph cache. You can see the formal verification running here in PR 101 against prospective EACL v8.0.

Aside: EACL v8.0 now supports multiple backends: Datomic Pro, Datahike and DataScript.