Artificial Intelligence

BAIF Launches 'Signal Shot' to Verify Signal Protocol Using AI

Is Signal Shot the dawn of provably secure communication or an impossible task?

APR 9·Updated APR 20

BAIF Launches 'Signal Shot' to Verify Signal Protocol Using AI

Story

Above: Signal app logo seen through a magnifying glass on Dec. 29, 2024. Image credit: Matthias Balk/Picture Alliance/Getty Images

The Facts

The Beneficial AI Foundation (BAIF), co-founded by MIT professor Max Tegmark and Tufts Researcher Meia Chita-Tegmark, on Monday launched Signal Shot, a formal verification project using Lean theorem prover and AI tools to produce a mathematical proof that Signal's encryption protocol is secure in both design and real-world code.
Beneficial AI Foundation
Lean
Formal verification uses mathematical proof to confirm a system cannot behave outside its specification and has previously been applied in aerospace and autonomous aviation. Though Signal has previously incorporated formal verification into its design, BAIF claims Signal Shot would represent its first application to a messaging protocol of this scale.
Association for Computing Machinery
Beneficial AI Foundation
Association for Computing Machinery
seL4
signal
BAIF states that Signal Shot will verify security by "writ[ing] down a mathematical model of the protocol and prov[ing] its security properties," before translating Signal's actual Rust code into Lean via a tool called Aeneas and proving it matches that model — producing a logical proof rather than a test result.
Beneficial AI Foundation
The initiative is organized by BAIF in partnership with Lean-focused group LeanFRO. AI will assist by "auto-formalizing research papers, expanding proof sketches into detailed verification plans" and "grinding through the tedious proof steps," work it describes as having previously been "bottlenecked by human effort."
Beneficial AI Foundation
Last year, AI-assisted mathematical reasoning achieved medal-winning scores for the International Maths Olympiad, while more recently Anthropic announced that an unreleased model, Claude Mythos, was highly effective at identifying software vulnerabilities and unsafe for public release due concerns it could be misused to exploit critical infrastructure.
Anthropic
Tom's Hardware
ByteDance
Nature
Signal underpins end-to-end encryption for over one billion users via its integration into WhatsApp in 2016. Gaps between verified design and implementation have previously led to large public data leaks, including the 2014 Heartbleed Bug, where a flaw in OpenSSL went undetected for years and compromised widely used cryptographic systems.
signal
signal
The Heartbleed Bug
FOX News
CNN
Beneficial AI Foundation

Sources Split

LEFT

CENTER

RIGHT

ESTAB
CRIT

CENTER

PRO
ESTAB

The Spin

Techno-optimist narrative

For decades, software security has meant chasing bugs faster than attackers. By combining AI with tools like Lean, Signal Shot aims to shift that paradigm toward mathematical certainty. If machines can scale formal proofs once limited by human effort, covering both protocol design and implementation details, provable guarantees could become practical. Signal Shot, therefore, stands to bring the long-promised vision of truly secure communication closer to reality.

Beneficial AI Foundation

Techno-skeptic narrative

Even the most rigorous proof cannot fully capture messy real-world systems. Signal runs across diverse devices, codebases and updates, where unmodeled edge cases can emerge. Heartbleed was a single rogue variable in an implementation nobody had formally modeled, rather than an inherent design flaw. Projects like Signal Shot may strengthen assurance, but full, end-to-end proof of real-world security remains an elusive, if not impossible, goal.