What compiling against z3 taught us about trusting provers

Aditya Kumar · 13 November 2026

TL;DR — Since June, the Vx compiler asks the z3 solver to prove contracts while it compiles. In five months we found no wrong answer from z3. Every bug was on our side of the pipe: the question we sent, how we read the answer, or how often we asked. For ten weeks, a machine without z3 passed every proof. In about 23,000 of 26,000 queries, z3 skipped a line with a type error and answered without it, and the tests still passed. Wrong facts, such as a fact that outlived its variable, let z3 prove false contracts, and the programs printed wrong answers. And one function asked z3 16,128 questions, each in a new process.

A contract states what a function needs and what it promises. Vx proves contracts at compile time with z3, an SMT solver from Microsoft Research. Two earlier posts, What comptime can do and Proving tensor indices at compile time, showed what such proofs catch. This post is about the work around the solver. It shows how Vx asks z3 a question, and what went wrong in the five months since 3 June.

How Vx asks a question

Here is a function with a contract:

fn add_one(x : i32) -> i32
requires x < 100
ensures return > x {
  return x + 1;
}

fn main() -> i32 {
  print(add_one(5));
  return 0;
}

To prove the ensures, the compiler, vxc, writes this text and sends it to z3. We saved it with a small script named z3, put first on PATH, that copies its input and then runs the real z3:

(set-option :rlimit 1000000)
(set-logic QF_LIA)
(declare-const |return| Int)
(declare-const |x| Int)
(assert (<= (- 2147483648) |x| (- 2147483648 1)))
(assert (< |x| 100))
(assert (= |return| (- (mod (+ (+ |x| 1) 2147483648) 4294967296) 2147483648)))
(assert (not (> |return| |x|)))
(check-sat)

The first three assert lines are facts, things the compiler knows. They say that x is an i32, that the requires holds, and that return is x + 1, wrapped to 32 bits. The last one says the opposite of the goal, the claim to prove. Here the goal is the ensures. Then check-sat asks whether some x makes every line true. z3 answers unsat: no such x exists. So the ensures holds for every input that the requires allows. Delete the requires and z3 finds x = 2147483647, where the sum wraps to a negative number. The build then stops with E8001.

Three details in that text each have a reason:

The mod on the third line. z3's integers have no largest value. Until 1 November, Vx sent x + 1 as it is. z3 then proved an ensures that overflow made false at run time (#982, and the example in the earlier post). Now +, - and * wrap at the width of their type.
The rlimit on the first line. It limits z3 to a million steps of work. A limit in seconds gives a different answer on a slower or busier machine. A limit in steps gives the same answer on every machine with the same z3. The proofs in our tests need at most about 6,000 steps. A million steps take between 0.5 and 2 seconds.
The order of the names. The compiler sorts the declarations, so a program gives z3 the same text in every run. A step limit gives the same answer only for the same text.

The text goes to z3 -in -smt2 over a pipe. The design discussion in June chose text over the z3 library, so that the compiler would not depend on one solver. Text has a second use: a person can read each query, and paste it into z3 to try it. The cost is a new process for each question. We come back to that cost at the end.

A missing z3 passed every proof

The first version, on 3 June, printed a warning when z3 was missing: "Skipping formal verification." Despite the message, the code reported each proof as failed. Two days later the tests failed on a CI machine without z3. The commit that fixed CI made the code match the message:

return Ok(false); // Return UNSAT so the proof trivially succeeds and compilation can continue

From then on, a machine without z3 built every program, and treated each contract as proved. By August the warning was gone too. The build printed nothing, and exited with status 0. We fixed it on 19 August, the day we found it (#374). A second path did the same until 3 September (#442). It proves facts about memory transfers between devices, under the flag --verify-seams. We found it while we measured the cost of those proofs. Without z3, one took 0.0031 ms, the time it takes to give up.

Today, a missing z3 stops the build:

Warning in add_one.vx: SMT solver error: no SMT solver available, so this condition could not be proved (No such file or directory (os error 2)). Vx runs `z3` to verify contracts, loop invariants, `Verified<T>` asserts and `raw::` bounds; install it (macOS: `brew install z3`, Ubuntu: `apt install z3`)
Error[E8001] at add_one.vx:4:3: Function 'add_one' cannot prove postcondition (ensures) at compile time
Error[E8006] at add_one.vx:8:9: this call to 'add_one' may not meet its precondition `x < 100`: the compiler cannot prove it from what is known here

The rule now: a proof that did not run is a failed proof.

The rule has a cost. z3 is optional for a program with no contracts, and the install guide says so. But the compiler proves a library contract again in each program that uses it. On 4 November, a change gave Vec::len the contract ensures return == self.len. We tried it with no z3 on PATH, and a program that called v.len() stopped with E8001 inside vec.vx. The fix, in the same change, proves three simple kinds of goal with no solver. They are a goal that is one of the facts, a goal of the form a <= a, and 0 <= b when a fact says b >= 0. The contracts of Vec hold in these ways, and a test compiles a program that uses Vec with no z3.

z3 answers in its own types

Every name in an SMT query has a sort, the solver's word for a type. Until 8 November, Vx declared every name as an Int, also a bool parameter. A bool used as a condition is then a sort error. This query asks whether x >= 1 when x is 1 or 2, depending on c:

(set-logic QF_LIA)
(declare-const |c| Int)
(declare-const |x| Int)
(assert (or (and |c| (= |x| 1)) (and (not |c|) (= |x| 2))))
(assert (not (>= |x| 1)))
(check-sat)

z3 4.15.4 answers:

(error "line 4 column 30: Sort mismatch at argument #1 for function (declare-fun and (Bool Bool) Bool) supplied sort is Int")
sat

z3 reports the error, skips that assert, and answers for the rest. Without the fact about x, the goal fails. Vx looked only for sat or unsat in the answer, so the proof failed with no visible cause.

A lost fact can make a proof fail, and it can never make one pass. No test needed a fact that z3 skipped, so every test stayed green. When we counted, about 23,000 of the 26,000 queries in the integration tests ended in a z3 error (#2987). The fix gives each name its sort, and treats any z3 error as a bug in the compiler: the compiler stops and prints the query. A compile of every .vx file in the tests, the standard library and the examples went from 11,665 queries with an error to none.

Stopping on every z3 error found the next mismatch at once. Take a comparison of floats, such as s > 0.0, in a branch where the compiler proves that an index is inside its tensor. It reaches z3 as an integer fact with a decimal number in it. z3 answers logic does not support reals, and the compiler now crashes (#3145, still open). Before the strict check, z3 dropped that fact too. We prefer the crash: it names the bug, with the query.

The logic has the same kind of limit. QF_LIA allows only linear arithmetic, so z3 refused row * dims + d, a product of two variables (#2849). Vx now asks for nonlinear arithmetic, QF_NIA, only when a fact needs it. And in a contract, a usize sum still has no upper limit in z3, while the program stops on overflow at run time (#2986, open).

z3 trusts the facts

The question is always the same: is there an input where every fact holds and the goal fails? z3 does not check the facts. A wrong fact can prove a false goal by itself. And if two facts contradict each other, no input makes every fact hold, so z3 answers unsat for every goal, true or false. So a wrong fact is worse than a missing one. A missing fact makes a true contract fail to prove. A wrong fact can make a false contract pass.

Most of our serious bugs had this shape. Here is one. The compiler kept the facts of a let after its block ended:

fn f(c : i32) -> i32
ensures return == 500 {
  let y : i32 = 1;
  if c > 0 {
    return 500;
  } else {
    let y : i32 = 500;
    print!("{} ", y);
  }
  return y;
}

fn main() -> i32 {
  println!("{}", f(-5));
  return 0;
}

The fact y == 500 from the inner let outlived the else block. At return y it described the outer y, which holds 1. The compiler proved return == 500, and the program printed 500 1 (#2406). Today it stops with E8001.

The same shape came back in other places:

A fact from before a loop held for the whole loop body, also after the body changed the variable. A call with requires n < 5 passed, and the program printed n=30; (#2619).
A fact about c.n survived a call that changed c through a &mut. The program printed n=10;, and a second case printed n=1000; (#2620).
An assert that the compiler could not decide became a run-time check and a fact. Inside a comptime block, the check went away with the block, and the fact stayed. A function with ensures return > 100 compiled, and the program printed 5 (#2034).
A for loop checked its invariant for the same i at the end of the body. The next pass has i + 1 (#2827).

We stopped two more before they reached main. When an assignment x = e became a fact, the old value of x needed a name. With one shared name, x = x + 1; x = x * 2; gives $old == $old + 1, which no number satisfies. So each old value gets a name of its own, and so does each loop exit.

Another time, we gave return the range of its type as a fact. It looked harmless. To test the wraparound, we broke it on purpose, and the wrong value of return fell outside that range. The two facts contradicted each other, so z3 proved the ensures anyway. The range hid the bug, so return gets no range of its own.

The rule now: a fact names one value, and it ends where that value ends. To test a change to the prover, we break each part of it on purpose, one at a time. Then we check that the test for that part fails. A test that stays green when its rule is broken checks nothing.

The price of a process

On an M4 Mac, the add_one query takes 4.5 ms in a new z3 process. The same query, sent 200 times to one z3 process, takes 1.5 ms each. So most of the time goes to starting z3. For add_one, vxc 0.0.4 starts z3 four times for two questions, because its default code generator checks each function twice.

We built the proofs about memory transfers with one z3 process from the start. Each question goes between a push and a pop, which save and restore the state of z3. A question costs about 55 µs (#433). The contract prover came first, and it still starts a process for each question.

That cost became visible this week. A write through a raw pointer gives a fact: these bytes are now set. Two writes side by side give two facts, and a proof about the whole range needs them joined. So on 6 November, each new write began to ask z3 whether its range touches the range of each earlier write. It asked in up to four ways. Each question was a new process. A function with N writes asked 4·N·(N−1) questions. Half of them came from the second time the default code generator checked the function:

Writes	z3 runs	Time
4	48	0.9 s
8	224	4.0 s
16	960	17.6 s
32	3,968	70 s
64	16,128	about 5 min

In the 8-write program, z3 answered sat to every one of these questions. No two ranges could be joined, because the offsets depend on a run-time number. A file of generated GPU kernels in glm-vx had up to 64 writes per tile. It did not finish in six hours. vxc used under a minute of CPU, and its z3 processes used about 5.6 hours (#3326).

The fix (#3327, in review) asks fewer questions. When two offsets differ by a whole number, such as k + 3 and k + 4, it compares them with no solver. So writes to p[0] through p[63] need no z3 at all. It asks one question first, "can these two ranges touch?", and skips the other three when the answer is no. And it asks about at most four earlier writes. The 64-write function went from 16,128 z3 runs to 492, and the file of kernels from more than six hours to under six minutes.

The next step is to start z3 less often: one process for each function, or the z3 library linked into the compiler (#375). On a Mac, vxc already links that library, through Homebrew's LLVM, and calls none of its functions.

What we keep

Text over a pipe. Each query is a file that a person can read and run. When z3 rejects one, the compiler prints it.
A missing z3 fails the build. A proof that did not happen must look different from a proof that passed.
A limit in steps. The same program gets the same answer on every machine.
No solver for the easy goals. A program with no contracts of its own should not need z3, so the contracts of the standard library must hold without it.
Every z3 error is a compiler bug. An error that z3 skips is a fact that Vx loses.
One value per fact. A fact that outlives its value can prove anything.

Still open: floats in a fact (#3145), usize overflow (#2986), an ensures about a returned struct (#1590), and one process for many questions (#375).

We compiled every program in this post with vxc 0.0.4 and z3 4.15.4 on an M4 Mac. The table comes from #3326, measured at commit 22a0a84f. Tell us about a contract that Vx could not prove, or one that it should not have, on r/vxlang.