AlphaProof Code verifiserer Signal helt ned i maskinkoden
AlphaProof Code har brukt AI-agenter til å verifisere sentrale deler av Signal helt ned i den kompilerte maskinkoden. Det er et skikkelig gjennombrudd. Ikke fordi en språkmodell sier at koden ser trygg ut, men fordi 6,5 millioner linjer med bevis er kontrollert av Lean og koblet til den kompilerte AArch64-koden i forskernes avgrensede libsignal-oppsett. Signal er allerede blant de mest granskede krypteringsprotokollene i verden.



