Insights from our audit practice, software releases, and applied cryptography research. Updated whenever we publish.
After 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 readCryspen said they'd be 'very interested' if someone found a bug in their verified code. We found three.
12 min readVerifpal 0.31.2 ships a major overhaul to active attacker analysis, finally enabling full verification of Signal's three-message protocol.
7 min readA case study on Cryspen's libcrux exposing the gap between formal verification marketing and engineering reality.
10 min read