31 gange hurtigere end Kani fra Amazon på samme bevis 0,285 s mod 8,895 s. Samme kode og grænser på en CPU kerne. Det midterste af 3 forsøg. Tre tjek af Nexagate. Ikke hele Rust.
Sådan virker den
Test tjekker de input, vi kom i tanke om. Fejl kan gemme sig i resten. Phage regner på alle input på en gang.
Den giver tre mulige svar: Koden er bevist. Her er et input, der giver fejl. Eller: Det ved jeg ikke. Den tjekker den kode, som faktisk bliver bygget.
Tre tjek af vores webserver
Vi kørte Phage og Kani fra Amazon på tre dele af Nexagate. Med samme kode og 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. En CPU kerne. Det midterste af 3 forsøg. Tre tjek af Nexagate. Ikke hele Rust.
Det fandt den
En gammel udgave af vores webserver gik ned, når en header havde et meget langt tal. Vi rettede fejlen. Phage beviste rettelsen for alle input op til 12 bytes.
Den førte os også til en fejl i LLVM, som bygger Rust kode. Fejlen er i 20.1, 21.1 og 22.1. Rettelse 195516 kom med i 23.1 den 3. maj 2026.
Det er tre tjek. Ikke hele Rust. Phage er stadig ny.