Google DeepMind did something unusual. It deliberately put two old security bugs back into Signal's encryption code, then asked AI to check whether something was wrong.
The AI caught both. It produced mathematical proofs showing the modified software failed to meet its security requirements.
On November 10, Google introduced AlphaProof Code, an AI system that generated roughly 6.5 million lines of mathematical proofs to check Signal's cryptographic code. Five researchers completed the project in four weeks. Similar verification work has historically taken teams of specialists years.
Now, here's why this is interesting.
What if developers could use AI to check whether their software is secure before hackers get a chance to exploit a vulnerability?
Google's experiment suggests it's becoming more realistic, although there's quite a bit the technology still can't check.
How does AI check software security using math?
When developers want to know whether their software is secure, they usually look for things that could go wrong. They might try to break into an account or see whether someone can intercept an encrypted message. If they find a problem, they fix it and test again.
Google's researchers took a different approach called formal verification. Here's how it works.
Say you're developing a messaging app, and you want to make sure nobody can read messages unless they're part of the conversation.
You could run thousands of security tests to see whether someone can get around the encryption.
Or you could describe the security requirement mathematically and prove that the software follows it across every situation covered by your mathematical model.
That's what formal verification is designed to do.
With AlphaProof Code, researchers worked with AI to turn Signal's security requirements into mathematical rules. Once those rules were reviewed, AI agents generated proofs using a system called Lean.
Think of Lean as a very strict math teacher. It checks every logical step, and if something doesn't add up, the proof gets rejected.
The AI can suggest a proof, but Lean decides whether the math actually works.
Google's researchers also checked about 140,000 instructions from compiled machine code. That's the version of the software a computer processor executes. This allowed them to examine whether the code followed the security requirements, rather than relying solely on how the software was originally designed.
Google put old security bugs back into Signal. Why?
Here's where the experiment gets more interesting.
The researchers wanted to know whether their verification system could recognize security problems that had already been discovered and fixed.
After all, getting a mathematical proof doesn't automatically mean you've checked everything that could go wrong. A proof might be perfectly valid while missing a security problem that researchers forgot to include in their requirements.
So Google brought back two previously fixed vulnerabilities in separate test versions of Signal's code. The first bug involved how the app handled sensitive information after certain messages failed to decrypt. Under specific conditions, the software could retain session information that should have been discarded.
The second involved how the software checked cryptographic keys. A specially modified key could cause the software to create another session using the same shared secret.
You don't need to understand the underlying cryptography to see why both problems were worth testing. They involved mistakes in how the software protected sensitive information.
When researchers ran the verification process on the modified versions, AlphaProof Code produced machine-checked proofs showing that the code violated its security requirements.
Both vulnerabilities had already been fixed in Signal. Google restored them specifically for this experiment. The result showed that AlphaProof Code could recognize the security failures associated with two real, previously discovered bugs.
So, what exactly did Google verify?
The researchers focused on the cryptographic technology that protects Signal's private conversations.
According to Google's technical paper, the work covered several security protections, including message confidentiality and authentication. Message confidentiality is what keeps outsiders from reading your encrypted conversations. Authentication helps ensure you're communicating with the intended person rather than someone pretending to be them.
The researchers also examined something called forward secrecy.
Let's say someone manages to steal one of the encryption keys used by your messaging app. Forward secrecy is designed to prevent that person from using the compromised key to read your earlier conversations.
Then there's post-compromise security, which allows a conversation to regain protection after an attacker temporarily accesses sensitive information, provided certain conditions are met. These protections explain why Signal was an interesting choice for the experiment. People depend on its encryption to keep private conversations private.
Signal CTO Ehren Kret welcomed the research. In Google's announcement, he explained that automated verification gives Signal greater confidence in the privacy protections provided by its implementation.
But before anyone concludes that Signal has now been mathematically proven completely secure, there's an important catch.
Does this mean Signal has no security vulnerabilities?
Google verified specific parts of Signal's cryptographic implementation, particularly the technology used to establish and protect one-to-one conversations.
The researchers didn't examine the entire Signal mobile app. Group messaging and communication across multiple devices weren't covered, either. They also didn't account for every possible way someone might exploit a device or gain access to sensitive information.
Here's another limitation worth understanding: a mathematical proof can only check the security rules researchers tell it to check.
Think about a banking app. Suppose developers mathematically prove that unauthorized users can't access someone else's account through the login system. That's reassuring. But what happens if another part of the app accidentally exposes customer information?
The original proof wouldn't catch it because the researchers were checking the login system, not every part of the application.
The same problem applies to Signal. Even if Lean confirms that a mathematical proof is correct, researchers still have to decide which security problems the proof should cover.
And that part takes considerable human effort.
In fact, Google's team said most of its work went into developing the mathematical specifications rather than generating the proofs themselves.
The researchers also relied on assumptions about certain cryptographic components. Their quantum-related findings covered specific protections rather than every possible threat from future quantum computers.
For anyone interested in examining the results, Google has published the proofs and specifications.
Could AI eventually check the security of everyday software?
Think about how many applications depend on software behaving exactly as intended.
A banking platform needs to prevent unauthorized transactions. A medical device needs to respond correctly to critical inputs.
A security mistake in either could have serious consequences, which is why mathematical verification could be valuable beyond encrypted messaging.
We've already seen AI become more capable of finding software vulnerabilities. As The Neuron previously reported, OpenAI's GPT-6 Cyber can discover security weaknesses and develop working exploits.
AlphaProof Code offers another way to examine software security. Developers could use AI to help prove that certain protections work as intended before releasing their code.
Of course, making this available to everyday development teams is another challenge.
Google hasn't disclosed how much the Signal experiment cost, and there's no commercial AlphaProof Code service available yet. There's also the question of what happens when developers update their software.
If a company changes thousands of lines of code every week, can AI keep checking the security requirements just as quickly? And how much would that cost?
Google still needs to answer those questions.
In an interview with WIRED, DeepMind researcher Swarat Chaudhuri acknowledged that considerable work remains before the technology can verify much larger software systems.
Still, completing this experiment in four weeks gives researchers something concrete to build on.
If AI can eventually make mathematical verification affordable enough for regular software updates, developers could have another way to catch serious security mistakes before those mistakes reach users.
