Applied cryptographer based in Paris. I audit cryptographic systems at Cure53 and run Symbolic Software, a boutique cryptography consultancy. I recently taught Applied Cryptography at the American University of Beirut, which required me to design a novel, highly ambitious and comprehensive curriculum from scratch, producing what I think is among the best introductory applied cryptography course curriculums and materials for an undergraduate university setting.
As a Senior Applied Cryptography Auditor at Cure53, I am a lead in the cryptography audit team, helping direct high-profile security assessments for major clients including Coinbase and other industry leaders. I have audited over 250 cryptographic systems, including end-to-end encrypted messaging applications, authentication protocols, key management systems, and cryptographic libraries.
I also serve as advisor to various organizations on sensitive cryptographic issues, providing expert guidance on protocol design, implementation security, and threat modeling.
I founded and direct Symbolic Software, a Paris-based software publisher and boutique applied cryptography consultancy. Since 2017, we have participated in over 250 software security audits for organizations ranging from Fortune 500 companies to critical open-source projects, and published research software tools used by the applied cryptography community.
seeking to return to teaching and research in 2026
I am actively seeking to return to academic research. While I have no interest in revisiting formal methods or the high assurance cryptography community, I am drawn to research directions that leverage my extensive auditing experience: analyzing real-world cryptographic deployments and their failure modes, post-quantum migration strategies for deployed protocols, high-performance cryptographic implementations, and the design of protocols that employ cryptographic primitives in novel ways.
My recent experience teaching Applied Cryptography at the American University of Beirut was deeply fulfilling. I designed a comprehensive curriculum from scratch that I believe represents one of the most rigorous introductory applied cryptography courses available at the undergraduate level. The experience reinforced my conviction that teaching is where I can make my most meaningful contributions. Understanding the cultural context and being able to integrate materials effectively for students navigating difficult circumstances gave the work a sense of purpose that I am eager to continue building upon.
I taught Computer Security at New York University Paris, where I introduced students to foundational concepts in security including threat modeling, cryptographic primitives, network security, and secure software development practices.
My research has focused on the formal verification of cryptographic protocols and their implementations. Early work contributed to the first formal verification of smart contracts and helped establish verified models for the TLS 1.3 standard candidate. I developed approaches combining symbolic and computational methods for automated verification of secure messaging protocols, which influenced the design of tools like Verifpal and Noise Explorer.
Other contributions include EverParse (verified zero-copy parsers for authenticated message formats), formal modeling of domain validation and the ACME protocol, analysis of the ProtonMail cryptographic architecture, and work on formally verified public ledger design. My Ph.D. thesis synthesized much of this work into a comprehensive treatment of formal verification for real-world cryptographic systems.
A full list of publications is available at Google Scholar.
I earned my Ph.D. at Inria Paris with the thesis Formal Verification for Real-World Cryptographic Protocols and Implementations.
Verifpal introduced a novel approach to symbolic analysis that balances usability with rigor, employing an intuitive modeling language that allows protocol designers and security practitioners to verify their constructions without requiring expertise in theorem provers or process calculi. Used by Google, Zoom, Bosch and others.
Noise Explorer provides comprehensive formal analysis and implementation generation for the Noise Protocol Framework, which underpins secure communications in applications like WhatsApp and WireGuard. The tool automatically generates formal models for any Noise handshake pattern, produces verified security proofs, and outputs ready-to-use implementations in multiple programming languages.
Kyber-K2SO is a clean, portable implementation of the Kyber post-quantum key encapsulation mechanism in Go. Designed for easy integration into existing projects, it provides a straightforward API for post-quantum secure key exchange.
folder.zone enables end-to-end encrypted, peer-to-peer folder sharing directly in the browser. Select a folder, receive a link, share it. Files are encrypted client-side with AES-256-GCM before transmission; the server never receives encryption keys. Currently in beta.
Dr. Kobushi's Labyrinthine Laboratory is an indie puzzle adventure game featuring over 100 levels. Published on Steam and Nintendo Switch.
Runes of Ardun reimagines the ancient Japanese strategy game Mini Shogi. Features an original AI written in Rust playing at 2200 Elo. Featured in Apple's New Games We Love; Top 10 Board Game in 20+ countries.
Piccolo: Othello is an Othello app for macOS and iOS written in Rust and Swift. Featured in Apple's What We're Playing, Games We Love, and Best Games Made in France. #1 game in the Japan Mac App Store, April–July 2021.
I am President and Editor in Chief of the Galactic Association for Cryptologic Research (GACR), a non-profit scientific organization for cryptology research that maintains the GACR ePrint Archive.
I host Cryptography FM, a podcast featuring conversations with researchers and practitioners about developments in cryptography, from theoretical advances to practical deployment challenges.