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.
Event details: buff.ly/YcuZTVB
π Protect your data against harvest-now-decrypt-later attacks with PSQ!
Weβve built a lightweight, hybrid post-quantum protocol that injects HNDL security into your existing protocols. The easiest way to start your post-quantum transition today without rewriting your entire stack.
buff.ly/irOf0lH
π Weβre growing! Cryspen is hiring.
Are you passionate about high-assurance software or cutting-edge cryptography? We are looking for talented individuals to join our team.
πΉ Compiler and Verification Tools Engineer
πΉ Cryptography Engineer
π Apply here: buff.ly/J9TF6NB
#Hiring #TechJobs
New blog post is live! π¦ We used hax and F* to formally verify termination and panic freedom for a small real-world Rust crate.
We also put Kani, Verus, and Aeneas to the test on the same code, exploring the different approaches, challenges, and proof efforts required by each tool.
buff.ly/h5bG37W
Catch Karthik, our Chief Researcher, at the European Conference on PQC Migration next week, where he will be championing the need for the EU to implement provably secure protocols and high-assurance software.
See you there? π
π
Dec 2-3, 2025
π buff.ly/w3XMpJQ
#PQC #EU
We're thrilled to welcome Alexander Bentkamp to the Cryspen family!
Alex joins our Tools and Proofs team with a deep background in automated and interactive theorem proving.
Welcome aboard, Alex!
buff.ly/jsJHshv
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.
buff.ly/UPf2MiN
β#AutomotiveSecurity #PQC #Crypto #SupplyChain
We are excited to share that Karthikeyan Bhargavan, co-founder and chief research scientist at Cryspen, will give a keynote talk at the PQCSA "PQC Migration & Supply Chain Readiness for the Automotive Industry" workshop (co-located with ESCAR in Frankfurt).
Excited to share our latest work on formally verifying the Rust standard library! We developed a new methodology to specify and test the Rust core library, helping to find and fix a bug in Rust's platform-specific SIMD functions.
Learn more about our approach: buff.ly/IwMkWVm
In Taipei for CCS 2025? πΉπΌ
Our CEO, Franziskus Kiefer, is giving a talk on Formal Security & Functional Verification of Crypto Protocols in Rust.
Don't miss the chance to connect. Franziskus is keen to discuss the future of secure software development and cryptography.
Attending the OpenSSL conference? π£οΈ
Our Chief Researcher, Karthikeyan Bhargavan, is giving a talk on high assurance post-quantum cryptography. He'd love to connect, so come find him for a chat about the future of crypto!
buff.ly/JIGSr0L
#OpenSSL #PQC #PostQuantum #Cryptography #Cybersecurity
We're excited to see the release of Signal's new post-quantum ratcheting protocol, SPQR!
We are proud to have collaborated with the Signal team on the formal analysis of the design and implementation of this.
Learn more on our blog buff.ly/Zi3rCBs and in Signal's announcement buff.ly/Srroli9
RWC 2026 will be held in Taipei between March 9 and 11, 2026, and Karthik is serving as one of the program committee chairs. Submissions are now open and the deadline is October 10th. So if you have something cool you're doing with crypto, submit a talk!
Submissions for RWC 2026 are open now!
Real World Crypto (RWC) is an annual event where cryptographers and security engineers can exchange ideas and results on the use of cryptography in mainstream applications.
buff.ly/0PoLe2D
How do we prove our cryptography is secure? π§
Join a talk by our Chief Researcher, Karthikeyan Bhargavan, on the rise of formally verified crypto!
#cryptography #formalverification #cybersecurity #PQC #infosec
JZLint 2.0 is here from MTG & Cryspen to lint post-quantum certificates! Now supporting ML-KEM & ML-DSA via libcrux.
Read more detail on the blog: buff.ly/EviQFar
#PQC #cryptography
Safer web browsing now possible thanks to spinout tech rooted in academic research. π
On #WorldWideWebDay note Karthikeyan Bhargavan & team at Inria who developed tools to improve cryptographic security online.
π europa.eu/!hP6t8w
#ERCPoC #AI #Cryptography #Encryption #WebSecurity
@cryspen.com
We're launching the embedded-cal project: Providing access to hardware accelerated and formally proven cryptographic algorithms on #embedded systems in #RustLang. For this, I'm teaming up with @inria Paris and @cryspen, supported by the #EU funded @NGIZero.
Right now we're going through [β¦]
As of today, XMTP is now a fully quantum-resistant decentralized messaging protocol.
This means, any developer, anywhere in the world can leverage XMTP to provide their users with private, decentralized, & quantum-resistant messaging.
We're proud to be recognized by Wavestone on their 2025 Radar of French Cybersecurity Startups.
A significant milestone that validates our core mission: building the essential developer tools for creating high-assurance software. Making provably secure software accessible to all developers.
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.
buff.ly/eEdJdnf
#Cloudflare #E2EE #VideoCalling #OpenSource #OpenMLS
The hax toolchain already supports several proof backends, including F*, Rocq, ProVerif, and SSProve. Give it a try hax-playground.cryspen.com
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.
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
At IEEE S&P, 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 MLS protocol. This work was done in collaboration with chief research scientist Karthikeyan Bhargavan.
Thrilled to welcome ClΓ©ment to Cryspen's Tools and Proofs team! π His expertise in formal methods (PhD from Inria Paris!) will be for conducting rigorous proofs and enhancing our tooling. Welcome, ClΓ©ment! π
#NewHire #FormalMethods
buff.ly/Ab4wuNA
Updates from some of Cryspen's Open Source Projects!
Check out our latest updates:
- Dive into the latest developments from the past month on π‘ππ±. buff.ly/trIZnTx
- And see how the ππ©ππ§πππ project is progressing and what's on the horizon. buff.ly/LAxrwnH
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, and how a a new OpenMLS feature makes fork resolutions a little easier.
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: buff.ly/fWGDzLY
#RustLang #CodeAnalysis #HighAssurance
Updates from some of Cryspen's Open Source Projects!
Check out our latest updates:
- Dive into the latest developments from the past month on π‘ππ±. buff.ly/TJpxWW1
- And see how the ππ©ππ§πππ project is progressing and what's on the horizon. buff.ly/VAJxltR
