Announcing CE Labs

CE Labs is a new Cryspen spin-off focused on Cryptographic Engineering.

Today, we are announcing the launch of CE Labs, a Cryspen spin-off dedicated to Cryptographic Engineering, under the leadership of Franziskus Kiefer. Learn more about CE Labs here. Going forward, …

EIC Transition: Spectrum

Cryspen has won an EIC grant to build a new software verification product.

We are excited to have been awarded a Transition Grant from the European Innovation Council to build a specification and verification toolkit that developers can use to build and deploy …

Software Verification in Lean

Cryspen is co-hosting a workshop on advancing software verification using the Lean proof assistant.

This week in Paris, Cryspen is delighted to be co-hosting Software Verification in Lean 2026, a workshop and associated hackathon organized by the Beneficial AI Foundation and the Lean FRO. SVIL 2026 …

The strengths and limits of formal verification

Getting precise about the guarantees of formal verification in our open-source libraries.

I have learned that it is important to be precise when documenting the guarantees offered by formally verified code, and to resist the temptation of simplifying things too much in trying to reach a …

PSQ: Post-Quantum Shared Secrets Made Easy

Announcing the PSQ protocol, a hybrid approach combining Diffie-Hellman and post-quantum KEMs to protect against harvest-now-decrypt-later attacks.

We’re pleased to announce the PSQ protocol for establishing a hybrid post-quantum shared secret between two parties. Cryptographic protocols, which exclusively rely on classical public key …

Cryspen Welcomes Alex

We welcome Alex to Cryspen

This month, we welcome Alexander Bentkamp (Alex) as the newest member of our team. Alex joins us with a strong background in automated and interactive theorem proving, where his passion for formal …

Formally Specifying and Testing the Rust Standard Library

Cryspen found and fixed bugs in the Rust SIMD libraries using formal specs

Modern programming languages typically come with a large standard library that implements essential language features like machine arithmetic and I/O, offers efficient data structures, provides …

Helping Secure Signal's Post-Quantum Transition

Cryspen worked with Signal to formally analyze their new post-quantum ratchet

Signal just announced the deployment of their new post-quantum ratcheting protocol, called the Sparse Post-Quantum Ratchet (SPQR), and Cryspen is proud to have contributed to the formal analysis of …

PQC Support for JZLint

MTG and Cryspen release JZLint 2.0: A tool for analyzing post-quantum certificates

We joined forces with MTG AG, a leader in public key infrastructures, to release JZLint 2.0 with support for analyzing post-quantum (PQC) certificates and their public keys. JZLint 2.0 is a …

• ««
• «
• 1
• 2
• 3
• 4
• 5
• »
• »»