Google DeepMind maakte op 10 nov 2026 bekend dat zijn nieuwe AI-framework AlphaProof Code is gebruikt om de daadwerkelijke code van het Signal-protocol formeel te verifiëren. Formele verificatie houdt in dat wiskundig wordt bewezen dat software precies werkt zoals bedoeld, zonder verborgen bugs. Het team begeleidde AI-agenten bij het opstellen en controleren van een bewijs dat de gecompileerde Signal-code belangrijke veiligheidsgaranties biedt, zoals dat berichten veilig blijven als een apparaat tijdelijk is gecompromitteerd. Het hele proces duurde vier weken; een klus waar expertteams normaal gesproken jaren voor nodig zouden hebben.
Wat AlphaProof Code doet
AlphaProof Code is een systeem met meerdere LLM’s (grote taalmodellen) die als agenten samenwerken. Menselijke onderzoekers vertalen de beveiligingsdoelen van Signal eerst naar formele specificaties en controleren elke stap. Daarna schrijft een groep agenten, aangestuurd door DeepMinds model Gemini Carbon, het bewijs in Lean, een taal waarmee wiskundige stellingen kunnen worden gecontroleerd. De agenten produceerden meer dan zes miljoen regels Lean-code en markeerden slechts ongeveer één procent van de codebase voor menselijke controle. Het systeem herkende ook correct twee eerder verholpen bugs toen die opnieuw werden geïntroduceerd. Dat laat zien dat het veilige code van code met fouten kan onderscheiden.
Waarom dit belangrijk is
De verificatie betreft de gecompileerde implementatie, niet alleen het ontwerp. Daarmee wordt een lacune gedicht waar veel kwetsbaarheden in de praktijk schuilgaan. Ehren Kret, de technisch directeur van Signal, zei dat het resultaat “meer vertrouwen geeft in de privacywaarborgen van onze code”. Experts zien dit als een stap naar AI die kan helpen om banken, medische apparaten, software voor elektriciteitsnetten en andere kritieke systemen met het hoogste beveiligingsniveau te controleren.
Waarom het ertoe doet
Voor gewone gebruikers betekent dit dat de versleuteling die miljarden berichten in Signal en Google Messages beschermt, op implementatieniveau wiskundig is gecontroleerd. Dat verkleint het risico op verborgen zwakke plekken. Voor ontwikkelaars laat het zien hoe AI-ondersteunde formele verificatie beveiligingscontroles kan versnellen. Hoe dit op grotere schaal werkt en wat het kost, is nog onduidelijk.
