We have launched a public challenge, to show people that verifying key components of a major application like Signal is doable today with existing tools. This is a similar effort to the Liquid Tensor Experiment, where a complex math theorem was formalized and proved with the help of the mathematics community, except that this time, we have the help of advanced AI models.

Elliptic-curve cryptography underpins much of modern security — from TLS handshakes to digital signatures to privacy-preserving tools such as Signal Messenger. Yet even carefully written, battle-tested cryptographic libraries can harbor subtle bugs that are nearly impossible to catch through testing alone. Our dalek-lite project takes a different approach: we use formal verification to provide machine-checked, mathematical guarantees that curve25519-dalek — one of the most widely used elliptic-curve cryptography library in the Rust ecosystem — behaves exactly as its mathematics demands.