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
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
escar Europe - The World's Leading Automotive Cyber Security
22. escar Europe - November 19 to 20, 2024, Dortmund (Germany)
escar.info
November 3, 2025 at 8:00 AM
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
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
Reposted by Cryspen
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).
October 27, 2025 at 10:45 AM
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
Learn more about our approach: buff.ly/IwMkWVm
Formally Specifying and Testing the Rust Standard Library
Cryspen found and fixed bugs in the Rust SIMD libraries using formal specs
cryspen.com
October 29, 2025 at 9:47 AM
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
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.
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.
ACM CCS 2025
This website requires JavaScript to function properly. Please enable JavaScript in your browser settings.
buff.ly
October 13, 2025 at 7:02 AM
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.
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
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
OpenSSL Conference Prague 2025 | October 7-9, 2025
OpenSSL Conference Prague 2025 | October 7-9, 2025
buff.ly
October 7, 2025 at 7:01 AM
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
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
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
Helping Secure Signal's Post-Quantum Transition
Cryspen worked with Signal to formally analyze their new post-quantum ratchet
buff.ly
October 6, 2025 at 7:01 AM
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
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
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
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
RWC 2026
Real World Crypto Symposium
rwc.iacr.org
September 18, 2025 at 9:02 AM
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
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
Join a talk by our Chief Researcher, Karthikeyan Bhargavan, on the rise of formally verified crypto!
#cryptography #formalverification #cybersecurity #PQC #infosec
High-Assurance Post-Quantum Cryptography OpenSSL Conference
Recent years have seen several landmark results in the formal verification of high-performance cryptographic libraries, leading to verified crypto code being adopted by mainstream projects like…
buff.ly
August 18, 2025 at 6:00 AM
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
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
Read more detail on the blog: buff.ly/EviQFar
#PQC #cryptography
PQC Support for JZLint
MTG and Cryspen release JZLint 2.0: A tool for analyzing post-quantum certificates
buff.ly
August 11, 2025 at 6:00 AM
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
Read more detail on the blog: buff.ly/EviQFar
#PQC #cryptography
Reposted by Cryspen
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
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
August 1, 2025 at 7:01 AM
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
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
Reposted by Cryspen
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 […]
Right now we're going through […]
Original post on chaos.social
chaos.social
July 15, 2025 at 3:17 PM
Reposted by Cryspen
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.
This means, any developer, anywhere in the world can leverage XMTP to provide their users with private, decentralized, & quantum-resistant messaging.
July 10, 2025 at 3:26 PM
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.
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.
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.
Radar des startups cybersécurité françaises 2025
Wavestone, en partenariat avec Bpifrance, a le plaisir de publier son Radar de l’innovation cybersécurité français 2025.
www.wavestone.com
July 9, 2025 at 6:56 AM
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.
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
buff.ly/eEdJdnf
#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
blog.cloudflare.com
June 30, 2025 at 5:52 AM
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
buff.ly/eEdJdnf
#Cloudflare #E2EE #VideoCalling #OpenSource #OpenMLS
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
#FormalVerification #Lean #Rust
June 17, 2025 at 4:38 AM
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
#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.
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…
buff.ly
June 10, 2025 at 1:20 PM
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
#NewHire #FormalMethods
buff.ly/Ab4wuNA
Cryspen Welcomes Clement
A Warm Welcome to Clement, Our Newest Cryspen Crew Member!
cryspen.com
May 14, 2025 at 5:22 AM
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
#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
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
This Month in Hax: April 2025 - hax
In April, we successfully merged 38 pull requests!
hax.cryspen.com
May 6, 2025 at 11:18 AM
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
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.
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.
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?
buff.ly
April 7, 2025 at 6:00 AM
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.
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
Read the full story: buff.ly/fWGDzLY
#RustLang #CodeAnalysis #HighAssurance
Redesigning Global Identifiers in hax - hax
A careful treatment of identifiers lies at the heart of all code analysis frameworks, and we hope our experience here proves useful to others.
buff.ly
April 3, 2025 at 6:00 AM
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
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
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
This Month in Hax: March 2025 - hax
In March, we successfully merged 32 pull requests!
buff.ly
April 1, 2025 at 10:34 AM
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
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
RWC 2025 buzzed with energy as the cutting edge of cryptography was presented to and discussed among an audience. Today, Cryspen teamed up with Google to showcase practical, scalable, verified solutions for high-assurance software and post-quantum cryptography.
Cryspen @ RWC 2025
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,…
buff.ly
March 27, 2025 at 12:59 PM
RWC 2025 buzzed with energy as the cutting edge of cryptography was presented to and discussed among an audience. Today, Cryspen teamed up with Google to showcase practical, scalable, verified solutions for high-assurance software and post-quantum cryptography.
New blog post! 📝 Control flow analysis with Hax. In this post we show how to ensure control flow properties such as "function A is always called before function B" in Rust. Super relevant for security! 🔒
buff.ly/ntTW299
#rustlang #formalverification #security
buff.ly/ntTW299
#rustlang #formalverification #security
Control flow analysis with hax
A difficulty of formal verification is that specifying programs can be hard. Certain kinds of programs can end up having a specification that is as complex as the code itself. In this case it is…
buff.ly
March 27, 2025 at 7:04 AM
New blog post! 📝 Control flow analysis with Hax. In this post we show how to ensure control flow properties such as "function A is always called before function B" in Rust. Super relevant for security! 🔒
buff.ly/ntTW299
#rustlang #formalverification #security
buff.ly/ntTW299
#rustlang #formalverification #security
Reposted by Cryspen
Thank you to new sponsors of Real World Crypto 2025, CASA, Chelpis Quantum, Cryspen, and Interop Labs! Your contributions are essential in making this conference possible and we look forward to seeing you in Sofia!
February 4, 2025 at 9:29 PM
Thank you to new sponsors of Real World Crypto 2025, CASA, Chelpis Quantum, Cryspen, and Interop Labs! Your contributions are essential in making this conference possible and we look forward to seeing you in Sofia!
Cryspen is heading to RWC in Sofia next week! 🚀 We'll be presenting "Using Formally Verified Post-Quantum Algorithms at Scale" and our team will be on hand to discuss all things high assurance software and crypto. Oh, and we're sponsoring too!
buff.ly/IC7eg8O
#RWC #Cryptography #PostQuantum
buff.ly/IC7eg8O
#RWC #Cryptography #PostQuantum
RWC 2025
Real World Crypto Symposium
buff.ly
March 18, 2025 at 9:11 AM
Cryspen is heading to RWC in Sofia next week! 🚀 We'll be presenting "Using Formally Verified Post-Quantum Algorithms at Scale" and our team will be on hand to discuss all things high assurance software and crypto. Oh, and we're sponsoring too!
buff.ly/IC7eg8O
#RWC #Cryptography #PostQuantum
buff.ly/IC7eg8O
#RWC #Cryptography #PostQuantum