This week in Paris, Cryspen is delighted to be co-hosting Software Verification in Lean 2026, a workshop and associated hackathon organized by the Beneficial AI Foundation and the Lean FRO.

SVIL 2026 brings together leading researchers and practitioners working on using the Lean proof assistant to formalize and verify real-world software. On Monday, I gave a talk on the challenges of verifying cryptographic applications, and the opportunities that are being opened up by the rapid innovations in Lean and by the emergence of AI-assisted formal proofs.

SVIL 2026 is initiating several exciting new collaborations. On Monday, BAIF and Lean FRO announced the Signal Shot, a challenge to the community to formally verify the Signal protocol and Signal app. Cryspen intends to contribute our tools and our expertise to this effort, in collaboration with our colleagues in the Aeneas team.

If you want to learn more about how Cryspen can help you build ambitious software with strong security and correctness guarantees, reach out to us.