Google DeepMind zegt de machinecode van het Signal-protocol formeel te hebben geverifieerd met AlphaProof Code

Pushmeet Kohli van Google DeepMind maakte bekend dat zijn team belangrijke beveiligingseigenschappen heeft bewezen van de machinecode waarop het Signal-berichtenprotocol draait. DeepMind zegt dat dit de eerste keer is dat de productiecode van een veelgebruikt protocol zo grondig formeel is geverifieerd, met welke methode dan ook. Dit zijn claims van DeepMind zelf.

Voor het werk gebruikte het team AlphaProof Code, dat DeepMind omschrijft als een nieuw agentisch raamwerk voor formele verificatie, dat draait op LLM's zoals Gemini Carbon. Volgens DeepMind reikt de verificatie tot aan de code die op apparaten draait en kostte het werk ongeveer een maand, terwijl vergelijkbare inspanningen teams tientallen jaren aan gezamenlijke inspanning zouden kunnen kosten. DeepMind noemt het Signal-team als partner.

DeepMind maakt de formele specificaties en verificatieartefacten open source, zodat anderen daarop kunnen voortbouwen. Het bericht had op de ochtend van 10 november 1.297 likes op X.