Cryspen

Recordings and slides from Software Verification in Lean 2026 are now available. The one-day workshop and multi-day hackathon, held in Paris in April, brought together researchers from the Beneficial AI Foundation, Cryspen, Ethereum Foundation, Google Research, Lean FRO, Microsoft Research and others to share recent advances, practical techniques, and ongoing challenges in building verified software. The workshop also included the launch of Signal Shot, a community effort to formally verify the Signal protocol and its Rust implementation using Lean. Max Tegmark, founder of the Beneficial AI Foundation, described the motivation simply: "Everybody should be able to be secure." 📺 Watch the recordings: https://lnkd.in/gGW8v7RF 📄 SVIL website: https://lnkd.in/g4dKUn8H 🔗 More about Signal Shot: https://lnkd.in/gCKWX-Nw #LeanLang #LeanProver #FormalVerification #SoftwareVerification

🔐 AI vs. Formal Verification: contradiction or complementary? Two powerful forces are reshaping software security: ➡️ AI-driven tools are unmatched at finding bugs fast. From zero-days in OpenBSD to vulnerabilities in FFmpeg that survived years of human fuzzing, AI tools like Claude‘s Mythos can now autonomously surface exploitable flaws across major systems. ➡️ Formal verification offers something AI alone cannot: a mathematical guarantee. CompCert and seL4 prove that when entire classes of vulnerabilities are eliminated by proof, there's nothing for AI (or hackers) to exploit. AI and formal verification are no competing approaches. Rather, they are converging. AI is now being used to accelerate formal proofs, while formal methods ensure critical infrastructure remains secure regardless of how advanced AI attacks become. For security-critical and cryptography-heavy code, the future isn't choosing between them. Rather, it's combining both. 📖 Want to dive deeper into how this intersection is evolving? Read the full piece below. #CyberSecurity #AI #FormalVerification #Cyberagentur #ClaudeMythos #trustworthyIT #TechInnovation #EVIT

Cryspen is co-hosting the Software Verification in Lean workshop and hackathon in Paris this week: https://lnkd.in/g4dKUn8H The workshop is organized by the Beneficial AI Foundation and the Lean FRO, and hosted by Inria and Cryspen. Lots of interesting discussions and collaborations between people working on Rust, Lean, Applied Cryptography, and AI-assisted proofs. Monday saw the launch of the Signal Shot challenge: https://lnkd.in/gbRVNvGz Beneficial AI Foundation Lean FRO Inria Signal Messenger

Alex will be speaking at Leaning In! 2026 in Berlin this Thursday, March 12. In his presentation, "Verifying security-critical Rust code with Lean," he will introduce Hax, Cryspen's toolchain for transpiling annotated Rust into monadic Lean code. The talk will explore how this approach leverages Lean's infrastructure to advance formal software verification, ensuring the correctness and reliability of security-critical systems. Event details: https://leaning.in/2026/ #LeanProver #RustLang #LeaningIn2026

Congrats to Cryspen 🏆   Cryspen received the POPL Most Influential Paper Award for their paper “Dependent Types and Multi-monadic Effects in F*”. The 2016 paper presented a redesigned version of F* enabling to work both as a proof assistant as well as a general-purpose, verification-oriented, effectful programming language. Karthikeyan Bhargavan received the award together with Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Z. and Santiago Zanella-Béguelin.   Today, F* plays a key role in Cryspen’s participation for PROTECT.     #POPL #EvIT #formalverification #trustworthyIT #cyberagentur

[🥇 Distinction] Le Most Influential Paper Award de la conférence #POPL2026 (Principles of Programming Languages) a été attribué à l’article « Dependent Types and Multi-monadic Effects in F* », co-signé par plusieurs scientifiques de l’équipe-projet PROSECCO du Centre Inria de Paris en 2016. Cette distinction récompense l’impact scientifique durable de ces travaux dans les domaines des langages de programmation et de la vérification formelle. En proposant une approche combinant types dépendants et effets multi-monadiques, l'article a contribué de manière déterminante au développement du langage F*. Ces recherches ont permis la mise en œuvre de projets dédiés à la vérification formelle de logiciels sécurisés à grande échelle. 👏 Félicitations aux auteurs, alors affiliés au Centre Inria de Paris lors de la rédaction : Catalin Hritcu (Max Planck Institute for Security and Privacy (MPI-SP), Karthikeyan Bhargavan (Cryspen), Chantal Keller (Centre Inria de Saclay), Antoine Delignat-Lavaud (Microsoft Research), Simon Forest (Centre Inria de l’Université de Lorraine), Jean Karim Z. (Direction de la Transformation Numérique (DTNUM), ainsi qu'à Cédric Fournet (Microsoft Research). © Tahina Ramananandro 📸

Nous recrutons (#hiring) pour le poste de Cryptography Engineer (Germany). Postulez dès maintenant ou partagez ce post avec votre réseau.

🚀 Protect your data against harvest-now-decrypt-later attacks with PSQ! We’ve built a lightweight, hybrid post-quantum protocol that injects HNDL security directly into your existing protocols. The easiest way to start your post-quantum transition today without rewriting your entire stack. 🛡️⚛️ Read the full announcement: https://lnkd.in/dVmC3Ekz #PostQuantum #Cryptography #Infosec #RustLang #HNDL

🚀 We’re growing! Cryspen is hiring. Are you passionate about high-assurance software or cutting-edge cryptography? We are looking for talented individuals to join our team and help us build the next generation of secure-by-design systems. 🔹 Compiler and Verification Tools Engineer 🔹 Cryptography Engineer Join us in our mission to make the digital world more secure. 👉 Apply here: https://lnkd.in/euh988wm #Hiring #Cryptography #FormalVerification #SoftwareEngineering #TechJobs

Delighted to win this year's Most Influential Paper award at POPL for our 2016 paper Dependent Types and Multi-monadic Effects in F*, along with Catalin Hritcu Chantal Keller Aseem Rastogi Antoine Delignat-Lavaud Simon Forest Karthikeyan Bhargavan Cédric Fournet Pierre-Yves Strub  Markulf Kohlweiss   Jean Karim Zinzindohoué and Santiago Zanella-Béguelin with thanks to all the many contributors to F*, Project Everest, and related projects over the years, and especially to Guido Martínez Tahina Ramananandro and Jonathan Protzenko, who have also been instrumental in developing F* over the years. The paper: https://lnkd.in/grzZPrde