Insights from our audit practice, software releases, and applied cryptography research.
Five proof-of-concept exploits against ML-DSA, ML-KEM, Ed25519, and ChaCha20 demonstrate three classes of semantic gap in hax's Rust-to-F* extraction pipeline, where verified models diverge from deployed code.
11 min readSymbolic Software is recommending post-quantum native design for all new cryptographic systems. This post examines the evidence behind that recommendation, its limitations, and the epistemic questions the industry should be confronting.
11 min readWe're opening 50 spots for students at Lebanese universities to take the Applied Cryptography course online, completely free of charge, starting June 2026. Applications are open now.
3 min readWe tested 15 ML-KEM and ML-DSA implementations across 5 languages, and found two conformance gaps and no security vulnerabilities.
4 min readWe're looking for a research intern to join us this summer and contribute to new papers on real-world cryptographic constructions.
3 min readAn examination of CE Labs' TLS implementations reveals 75% of valid ECDSA signatures rejected, authentication tags silently dropped, no certificate validation, and remote denial-of-service vectors.
11 min readVerifpal's analysis engine has been redesigned with a unified equational theory, provenance-tagged values, a formally grounded deduction loop, and a bounded-depth search that runs 3x faster, plus updated tooling across the board.
11 min readVerifpal now runs entirely in the browser via WebAssembly. The new Workbench at verifpal.com/workbench lets anyone write, verify, and visualize cryptographic protocol models with zero installation.
3 min readAfter seven years in Go, Verifpal has been completely rewritten in Rust, gaining a new analysis engine, massive performance improvements, a rich terminal interface, and a novel attack strategy that finds more attacks.
9 min readWe've updated Noise Explorer to address two bugs in generated Rust and WebAssembly implementations of Noise Protocol Framework handshake patterns.
2 min readThree findings in libcrux's ML-DSA implementation: a verifier norm check that is dead code due to a wrong constant, a missing bounds check in hint deserialization, and a wrong multiplication specification that renders AVX2 proofs unsound.
12 min readCE Labs said they'd be 'very interested' if someone found a bug in their verified code. We found three.
13 min read