Mastodawn

We're proud to be recognized by Wavestone on their 2025 Radar of French Cybersecurity Startups.

This recognition is a significant milestone that validates our core mission: building the essential developer tools for creating high-assurance software and formally verified cryptography. Making provably secure software accessible to all developers.

Full report (French): https://www.wavestone.com/fr/insight/radar-des-startups-cybersecurite-francaises-2025/

#Cybersecurity #Startup #DeepTech #DeveloperTools #FormalVerification #Cryptography #HighAssurance

Cryspen Jun 30

Cloudflare has launched Orange Me2eets, an open-source end-to-end encrypted video calling demo! Built on top of our OpenMLS implementation, this project showcases secure, private real-time communication.

https://blog.cloudflare.com/orange-me2eets-we-made-an-end-to-end-encrypted-video-calling-app-and-it-was/

#Cloudflare #E2EE #VideoCalling #OpenSource #OpenMLS

Orange Me2eets: We made an end-to-end encrypted video calling app and it was easy

Orange Meets, our open-source video calling web application, now supports end-to-end encryption using the MLS protocol with continuous group key agreement

The Cloudflare Blog

Cryspen Jun 18

chrysn Jun 17

Lakers, an implementation of #EDHOC, i.e., lightweight security for #IoT, now uses formal verification to continuously check a first small part of its code using #hax and F*, proving our buffers won't reach out of their bounds and panic. Thanks @cryspen for making that tool rather straightforward to learn.

Cryspen Jun 17

Cryspen is excited to announce it has been awarded a grant from the Ethereum Foundation to extend our hax verification toolchain with support for the Lean prover. Watch this space for more on this soon!

#FormalVerification #Lean #Rust

Show thread

Cryspen Jun 17

With the support of this grant, Cryspen will release a new version of hax that can translate Rust source code to purely functional models in Lean, enabling users to mathematically prove the correctness of their code using the increasingly popular Lean proof assistant.

The hax toolchain already supports several proof backends, including F*, Rocq, ProVerif, and SSProve. Give it a try https://hax-playground.cryspen.com/

Hax Playground

Cryspen Jun 10

At IEEE S&P in May 2025, Théophile Wallez presented new results on the formal security verification of a bit-precise executable specification of TreeKEM, the core key agreement component of the Messaging Layer Security protocol. This work was done in collaboration with Karthikeyan Bhargavan, our chief research scientist and one of Théophile's PhD supervisors.

https://eprint.iacr.org/2025/410

#MLS #Cryptography

TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security

The Messaging Layer Security (MLS) protocol standard proposes a novel tree-based protocol that enables efficient end-to-end encrypted messaging over large groups with thousands of members. Its functionality can be divided into three components: TreeSync for authenticating and synchronizing group state, TreeKEM for the core group key agreement, and TreeDEM for group message encryption. While previous works have analyzed the security of abstract models of TreeKEM, they do not account for the precise low-level details of the protocol standard. This work presents the first machine-checked security proof for TreeKEM. Our proof is in the symbolic Dolev-Yao model and applies to a bit-level precise, executable, interoperable specification of the protocol. Furthermore, our security theorem for TreeKEM composes naturally with a previous result for TreeSync to provide a strong modular security guarantee for the published MLS standard.

IACR Cryptology ePrint Archive

Cryspen May 14

Thrilled to welcome @blement to Cryspen's Tools and Proofs team! 🎉 Clément's expertise in formal methods (PhD from Inria Paris!) will be for conducting rigorous proofs and enhancing our tooling. Welcome, Clément! 🚀

#NewHire #FormalMethods

https://cryspen.com/post/welcome_clement/

Cryspen | Cryspen Welcomes Clement

A Warm Welcome to Clement, Our Newest Cryspen Crew Member!

Cryspen May 6

Updates from some of Cryspen's Open Source Projects!

Check out our latest updates:
- Dive into the latest developments from the past month on 𝐡𝐚𝐱. https://hax.cryspen.com/blog/2025/05/05/this-month-in-hax-april-2025/
- And see how the 𝐎𝐩𝐞𝐧𝐌𝐋𝐒 project is progressing and what's on the horizon. https://blog.openmls.tech/posts/2025-05-06-this-month-in-openmls/

This Month in Hax: April 2025 - hax

Cryspen Apr 7

MLS Group State Forks: What, Why, How

Group state forks are faulty states that MLS groups can end up in. We have a new blog post that looks at what they are exactly, how that happens and how to resolve them. We also look at a new OpenMLS feature that makes fork resolutions a little easier.

Get all the details on our blog: https://cryspen.com/post/mls-fork-resolution/

Cryspen | MLS Group State Forks: What, Why, How

What are state forks, why can’t they happen but do anyway and how can they be resolved in OpenMLS?

Cryspen Apr 3

Rust identifiers, demystified! We're revealing our analysis toolchain's secrets in our latest blog. Discover how we tackle global vs. local identifiers for better formal verification with hax.

Read the full story: https://hax.cryspen.com/blog/2025/04/01/redesigning-global-identifiers-in-hax/

#RustLang #CodeAnalysis #HighAssurance

Website	https://www.cryspen.com/
Github	https://github.com/cryspen