| Website | https://www.cryspen.com/ |
| Github | https://github.com/cryspen |
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/
New blog post is live! ๐ฆ We used hax and F* to formally verify termination and panic freedom for a small real-world Rust crate (gcd).
But that's not allโwe also conducted a deep comparative analysis! We put Kani, Verus, and Aeneas to the test on the exact same code, exploring the different approaches, challenges, and proof efforts required by each tool. See how the Rust verification landscape stacks up!
https://hax.cryspen.com/blog/2025/12/08/verifying-a-real-world-rust-crate/
Headed to #escar this week?
โCatch Franziskus talking high assurance crypto. And don't miss Karthik's keynote at the "PQC Migration & Supply Chain Readiness" workshop.
Lets connect and talk #verification and #cryptography.
How do we prove our cryptography is secure? ๐ง
Join a talk by our Chief Researcher, Karthikeyan Bhargavan, on the rise of formally verified crypto! Learn how libraries like HACL* & libcrux are securing Firefox, Signal & OpenSSH with formally verified guarantees, even against quantum computers. ๐ก๏ธ
We'll cover recent breakthroughs, challenges, and a vision for verifying giants like OpenSSL.
#cryptography #formalverification #cybersecurity #PQC #infosec
https://cfp.openssl-conference.org/openssl-conference-2025/talk/NPWQHG/
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
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! ๐
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.