Károly Zsolnai-Fehér describes research using AI agents and the Lean proof language to verify properties of code implementing the Signal encryption protocol. The work checks implementation against formal specificationsFormal verification uses precisely stated properties and logical methods to check whether a system or argument satisfies those properties. rather than relying only on a mathematical description.
He discusses forward secrecy and recovery after certain compromises, under the researchers’ security-model assumptions. The team also tested the approach by reintroducing two known bugs, and used separate checks to catch agents that changed a theorem into an easier claim.
Károly Zsolnai-Fehér notes that the proofs do not cover the whole application or group chats and assume underlying cryptographic primitives are secure. The work therefore does not establish that Signal cannot be hacked.
Watch on YouTube
