Cryspen is now pereq

A new name for the next chapter.

A few months ago, we announced that we were spinning off our cryptographic engineering projects to focus on building a new product funded by our EIC Transition grant.

Developer-driven Rust verification using hax, Lean, and AI

Showcasing hax 0.4 on IoT-friendly SHA-3

As announced in our recent blog post, hax 0.4 has a new Lean backend that relies on Aeneas. In this post, we describe how we used this new backend to verify the SHA-3 implementation in libcrux-iot, an …

Hax 0.4!

Announcing hax 0.4, a pivotal release

The world of mathematics has been shaken by an earthquake: LLMs can now generate large Lean developments autonomously: Navier-Stokes solution, FLT proof, and many more. The narrow stream of proof-work …

Paula Joins Cryspen

Cryspen welcomes Paula Grandía as our new Head of Operations

Cryspen is pleased to welcome Paula Grandía as our new Head of Operations, joining the team in August 2026. Paula brings an operations philosophy built around a simple idea: the best operational work …

Tobias Joins Cryspen

Cryspen welcomes Tobias Reiher as our newest verification engineer

We’re excited to announce that Tobias Reiher has joined Cryspen in July. Welcome, Tobias! Throughout his career, Tobias has worked on security- and safety-critical systems where software …

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 …

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, …

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 …

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