Test finder de fejl, vi kom i tanke om at lede efter. Phage regner på alle input op til en valgt størrelse. Den kan svare: Koden er bevist. Her er et input, der giver fejl. Eller: Det ved jeg ikke.
Tre tjek af vores webserver
Vi testede tre dele af Nexagate med Phage og Kani fra Amazon. Samme kode og samme grænser.
| Tjek | Svar | Phage | Kani | Hurtigere |
|---|---|---|---|---|
| QUIC tal, alle input op til 8 bytes | Bevist | 0,285 s | 8,895 s | 31,2 gange |
| Læsning af HTTP/2 headers, gammel udgave | Fandt en fejl | 2.326 s | 8.268 s | 3,6 gange |
| HTTP/2 headers, rettet, alle input op til 12 bytes | Bevist | 1.561 s | 6.078 s | 3,9 gange |
Samme kode og grænser på en CPU kerne. Det midterste af tre forsøg. Begge værktøjer var enige. Det dækker tre tjek. Ikke hele Rust.
Fejlen
Det andet tjek var af gammel kode, som læser HTTP/2 headers. Phage fandt en fejl på 2.326 s med et tal, som sprængte grænsen. Vi prøvede inputtet i det rigtige program. Det gik ned. Det er en fejl, vi vil finde før andre.
Vi rettede fejlen. Phage beviste rettelsen for alle input op til 12 bytes på 1.561 s. Det hurtigste tjek læser tal i QUIC beskeder. Det tog 0,285 s mens Kani brugte 8,895 s. Det er 31,2 gange hurtigere.
Også en fejl i LLVM
Phage tjekker den kode, som faktisk bliver bygget. I en test svarede den, at den ikke vidste det. Det førte os til en fejl i LLVM. Et trin, der holdt et tal lille, blev fjernet. Men løftet om et lille tal blev stående. Kani tjekker før LLVM og ser derfor ikke fejlen.
Fejlen findes i LLVM 20.1, 21.1 og 22.1. Den er rettet i LLVM 23.1 med rettelse 195516, som kom med den 3. maj 2026. Vi oprettede derfor ikke en ny rapport. Rust 1.94, som vi brugte, indeholder LLVM 21.
Det gælder mere end servere
Vi bygger også meget andet. Men vanen er den samme. Når fejl kan koste dyrt, vil vi have mere end test. Det gælder data udefra, penge og adgang. Her bruger vi bevis.