| Website | https://www.cryspen.com/ |
| Github | https://github.com/cryspen |
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.
@chrysn There are many reasons users may choose to use a specific backend, including familiarity and taste, but the most likely application is to link the proofs they do on Rust code via hax to existing proof developments in the chosen backend, e.g. some math library that only exists in that backend.
Using F* allows you to connect your proofs with HACL* and DY*; using Rocq allows connections with Jasmin and Bedrock; using Lean will allow you to connect your proofs with mathlib and with ongoing formalizations in the Ethereum ecosystem.
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!
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/
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.
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.
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! 🚀
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/
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/
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/
chrysn