Google touts AI breakthrough, path to "unhackable" software
Add Axios as your preferred source to
see more of our stories on Google.
Illustration: Sarah Grillo / Axios
Google DeepMind researchers have used AI to mathematically prove that the encryption code protecting billions of private messages works as intended.
Why it matters: The research breakthrough could eventually help defenders build better software. "You can finally get to this world of unhackable software," said Swarat Chaudhuri, a research scientist at Google DeepMind.
Driving the news: Google DeepMind said Tuesday it used AI agents powered by its Gemini 4 Carbon model to mathematically verify that the code underpinning Signal's encryption is secure.
- The agents generated more than 3 million lines of mathematical proofs in the process, allowing researchers to verify the software at a level of detail previously considered impractical.
- To test the system, researchers reintroduced two previously fixed bugs into Signal's code. In both cases, the AI-powered framework generated mathematical proofs showing that the altered software was insecure.
The intrigue: But Chaudhuri told Axios that the AI lab's tools were able to accomplish this feat in just four weeks — compared to the years it would've likely taken humans alone.
The big picture: The breakthrough could eventually help cybersecurity defenders move from hunting for bugs to mathematically proving they don't exist.
- Many security flaws emerge because the code running on a device doesn't behave exactly as its developers intended.
- Chaudhuri said the same technology could eventually help developers prove their software is protected against common weaknesses, including memory safety bugs that hackers routinely exploit.
What to watch: DeepMind is eyeing ways to integrate this new verification technology into AI coding agents and software development workflows, potentially allowing developers to mathematically verify security protections as they build and update software.
- Chaudhuri said the team is also exploring how to combine its research with Google's existing vulnerability-hunting and patching tools, including Project Zero and CodeMender.
- For now, the latest feat remains a research project, not a commercially available cybersecurity product.
