Tests check the inputs someone thought of. Bugs live in the ones nobody did. That is why we built Phage, a code prover for Rust. It considers every input a function can get, up to a size we choose, by reasoning about all of them at once instead of trying them one by one. Then it gives one of three answers. The code is proved, or here is an input that breaks it, or it does not know.
Three checks on our own web server
We pointed it at three parts of Nexagate, our web server, and ran the same checks with Kani, Amazon’s Rust checker, on the same code and with the same limits.
| Check | Answer | Phage | Kani | Faster |
|---|---|---|---|---|
| QUIC number reader, every input up to 8 bytes | Proved | 0.285 s | 8.895 s | 31.2 times |
| HTTP/2 header decoder, old version | Found a bug | 2.326 s | 8.268 s | 3.6 times |
| HTTP/2 header decoder, fixed, every input up to 12 bytes | Proved | 1.561 s | 6.078 s | 3.9 times |
Same code and limits on one CPU core, the middle result of three full runs. Both tools agreed on every answer. These are three checks, not every Rust feature, because Phage is still young.
The bug
The second check is an old version of the part of Nexagate that reads HTTP/2 headers. Phage did not prove it. It came back in 2.326 s with an input that breaks it, a header with a number so long that the math overflows. We sent that input to the real program, and it crashed. In a server, a crash that anyone can cause with one bad header is exactly the kind of bug you want to find before someone else does.
We fixed it, and Phage proved the fixed version for every input up to 12 bytes, in 1.561 s. Its fastest check, on the part that reads numbers in QUIC messages, took 0.285 s where Kani took 8.895 s. That is 31.2 times faster.
A bug in the compiler, too
Phage checks the code the compiler actually makes, not only the code we write. On one of its own tests, it answered that it did not know, instead of guessing. That answer led us to a real bug in LLVM, the engine inside the Rust compiler. One of the shortcuts LLVM takes to make code faster removes a step that kept a number small, but keeps the promise that the number is small. Kani checks the code at an earlier stage, before LLVM runs, so it never sees the bug.
LLVM 20.1, 21.1 and 22.1 have the bug. LLVM 23.1 does not, because LLVM had already fixed it in pull request 195516, merged on 3 May 2026. So we did not file a new report. Rust 1.94, the compiler we checked against, ships LLVM 21.
Why it matters beyond a web server
Most of what we build is not a web server. The habit carries over all the same. The parts of a system where a mistake is expensive, like reading outside data, money and who may do what, deserve more than tests. Proof is how we make sure.