| Website | https://www.cryspen.com/ |
| Github | https://github.com/cryspen |
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/
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/04/01/this-month-in-hax-march-2025/
- And see how the ππ©ππ§πππ project is progressing and what's on the horizon. https://blog.openmls.tech/posts/2025-04-01-this-month-in-openmls/
Real World Crypto 2025 buzzed with energy as the cutting edge of cryptography was presented to and discussed among an audience of leading researchers and developers from academia and industry. Today, on the second day of the conference, Cryspen teamed up with Google to showcase practical, scalable, verified solutions for high-assurance software and post-quantum cryptography.
chrysn