Compile-time verification with negative overhead

June 24, 2026

Most verified software pays a performance tax at compile time. Salt's verifier does the opposite. Adding a Z3 theorem prover to the compiler made compilation faster—not in spite of the proofs, but because of them.

Dafny extracts to C# after the proofs are done. F^* compiles to OCaml through a chain of intermediate languages whose verification artifacts are discarded before code generation. SPARK requires a separate verification harness that runs alongside the build. Each of these is a serious achievement. Each also adds a compile-time cost—sometimes by minutes, occasionally by hours. This is accepted as the price of correctness.

Salt takes a different approach. The theorem prover is not a separate tool. It is a compiler pass. It runs during normal compilation, operates under a strict time budget, and its output feeds directly into the optimization pipeline. The result is not zero-overhead verification. It is negative-overhead verification: the proofs make the compiler faster.

How it works

Salt is a systems language that targets MLIR and LLVM. Its syntax will feel familiar if you have written Rust or C. The one unusual feature is that functions can carry requires and ensures clauses—preconditions and postconditions checked by Z3 at compile time.

A binary search:

fn binary_search(arr: &[i64], target: i64) -> i64
    requires(arr.len() > 0)
{
    let mut lo: i64 = 0;
    let mut hi: i64 = arr.len() - 1;
    while lo <= hi {
        let mid = (lo + hi) / 2;
        if arr[mid] == target { return mid; }
        if arr[mid] < target { lo = mid + 1; }
        else { hi = mid - 1; }
    }
    return -1;
}

When the compiler encounters requires(arr.len() > 0), it translates the condition into a Z3 formula, negates it, and asks: can this ever be violated? Three outcomes are possible.

UNSAT. The negation is unsatisfiable. The condition holds for all inputs. Z3 has proved it. The compiler removes the check from the output entirely—no branch, no assertion, no instruction. The proof is the check.

SAT. Z3 found a counterexample. You get the specific values that would violate the contract before your program runs. The error message names the call site and the failing values. Fix the call site or widen the contract.

TIMEOUT. Z3 cannot decide within 100 milliseconds. This happens with non-linear arithmetic, deep loop nests, or path explosion. The compiler emits a runtime assertion. The program still compiles, still runs, still has defined behavior. Verification is progressive: you add the contracts you can prove today, and the rest become runtime checks you can address later.

The time budget is the critical design decision. A 100ms cap means verification never stalls a build. It means you can add contracts without fear of CI timeouts. And it produced a second-order effect we did not anticipate.

The surprise

We expected verification to add overhead. It removes it.

Compiling with verification is faster than compiling without it, and the output is byte-identical. The mechanism is straightforward: when Z3 proves a condition, the compiler eliminates the code path—the branch, the bounds check, the panic handler. Fewer instructions through MLIR and LLVM means less work for every downstream pass. The proof simplifies the intermediate representation before optimization begins.

This holds consistently across modules:

Sub-second feedback for all modules. You edit a contract, recompile, and the solver responds before you finish reading the next function.

Does it hold up on real code

LETTUCE is a Redis-compatible key-value store written in Salt. Nine commands, 314 lines of application code. The RESP protocol parser, command dispatcher, and append-only file persistence layer all carry Z3 contracts.

We ran it against Redis 7 on the same machine, using the same redis-benchmark tool, on the same SET workload, across 13 concurrency levels:

LETTUCE leads at every concurrency level. We swept from 1 to 100 clients in increments of 5; there is no crossover. A single-threaded event loop outperforming a multi-threaded production database on its own benchmark was not the result we expected.

The explanation is not CPU throughput. It is allocation. Redis calls zmalloc and zfree on every command. Under concurrent load, the allocator contends on arena locks. More clients, more contention, more time spent in malloc. LETTUCE has no heap allocations on the request path. The RESP parser returns StringView pointers into the receive buffer—zero-copy. The key-value store is backed by an arena: all keys and values live in a bump-allocated region, freed in O(1) by resetting a pointer. The response is written to a stack buffer. One allocation per connection (the session buffer), zero per request.

What the solver cannot do

Being precise about limitations is as important as presenting results.

Non-linear arithmetic. Z3 is primarily a linear solver. It can handle multiplication — machine integers are bounded, and Z3 has a non-linear strategy and bit-blasting — but proofs involving products of unknowns are much more expensive than linear ones. The practical advice is to give the solver linear constraints it can chain. Write requires(i < n && stride * n + offset < buf.len()) — two linear checks, both fast — instead of requires(i * stride + offset < buf.len()), which forces the solver into a more expensive strategy. Bounding your variables almost always makes the proof possible. Leaving them unbounded and multiplied together is what causes timeouts.

Path explosion. A function with many branches produces an exponential number of solver paths. The 100ms budget means deeply branching functions get runtime assertions on the unprovable paths rather than compile-time proofs on all of them. We believe this is the correct trade for a systems language: fast builds with partial coverage rather than complete coverage with slow builds.

External state. Z3 reasons about code, not the world. A contract that depends on filesystem state or network conditions cannot be checked by the solver. Contracts are most effective on in-memory data structures, array bounds, and arithmetic invariants.

None of these prevent compilation. When the solver cannot prove a contract, Salt inserts a runtime assertion. The verification is progressive: you add the contracts you can prove today, and the rest remain as runtime checks until you or the solver improve.

Getting started

Salt is open source. The compiler is written in Rust and produces native arm64 and x86-64 binaries through MLIR and LLVM.

git clone https://github.com/bneb/lattice.git
cd lattice
make build              # Build the compiler
make lettuce-verify     # Run 4 contract verification tests
make bench              # LETTUCE vs. Redis comparison

A tutorial walks through building a verified server from scratch. The benchmark methodology and raw data are published. The playground lets you try Salt in a browser. Everything is at github.com/bneb/lattice.