Google DeepMind researchers have successfully utilized agentic AI to mathematically prove the cryptographic guarantees of the Signal protocol, based on information published by Ars Technica.
The project, completed in four weeks, used a new framework called AlphaProof Code to formally verify the software. Formal verification uses mathematical proofs to ensure code functions as intended without critical vulnerabilities. While the researchers did not discover new flaws in the current protocol, the tool correctly identified known vulnerabilities in older versions of the software. This development represents a significant milestone in software security, as it demonstrates how AI can accelerate the labor-intensive process of verifying complex codebases. Although the results are promising, experts note that scaling this technology to entire software supply chains remains a challenge. Google DeepMind emphasized a human-AI collaboration model, where agents self-correct while maintaining human oversight at critical stages. The Signal Foundation, which has previously conducted its own verification efforts, welcomed the findings as a way to bolster confidence in privacy guarantees. As AI-driven security threats evolve, the industry is closely watching whether such automated verification can become a practical, cost-effective standard for banks and other high-stakes sectors.
Source: Ars Technica
