| 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/
🚀 Protect your data against harvest-now-decrypt-later attacks with PSQ!
We’ve built a lightweight, hybrid post-quantum protocol that injects HNDL security directly into your existing protocols. The easiest way to start your post-quantum transition today without rewriting your entire stack. 🛡️⚛️
Read the full announcement: https://cryspen.com/post/psq-announce/
🚀 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 and help us build the next generation of secure-by-design systems.
🔹 Compiler and Verification Tools Engineer
🔹 Cryptography Engineer
Join us in our mission to make the digital world more secure.
👉 Apply here: https://join.com/companies/cryspen
#Hiring #Cryptography #FormalVerification #SoftwareEngineering #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 (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/
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
🔗 https://pqc-conference.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, especially with the Lean proof assistant. We're excited to have his expertise as we continue our work on formally verifying security-critical software.
Welcome aboard, Alex!
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.
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: https://cryspen.com/post/specify-rust-simd/
In Taipei for CCS 2025? 🇹🇼
Our CEO, Franziskus Kiefer, is giving a talk on Formal Security & Functional Verification of Crypto Protocols in Rust.
If you're attending, don't miss the chance to connect. Franziskus is keen to discuss the future of secure software development and cryptography. Come and talk to him after his session!
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!
https://openssl-conference.org/speaker-sessions/detail-160_1292973#sectionLink
