16 posts in category “Research”.
Across 62 head-to-head benchmarks against hpke-rs, hpke-ng wins 43 — including ML-KEM decap at 53–55% faster, X-Wing decap at 38%, X25519 decap at 41%, and every post-quantum encap/decap row a clean win — ties 14, ships a 30% smaller binary, and a type system that catches four classes of bug at compile time.
21 min readA 52-page practitioner guide for engineers and architects working on post-quantum migration, alongside an interactive scorecard and TLS scanner at pq-migration.symbolic.software.
1 min readVerifpal 0.51.0 tightens the analysis engine's treatment of password-qualified values, checked ASSERT? assertions, and AEAD associated data, all on the back of excellent bug reports from the community.
7 min readWhy Symbolic Software agrees with Soatok's position on hybrid post-quantum constructions: hybrids are compelling for KEMs, far less necessary for signatures, and the real risk is migration friction.
6 min readFive 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.
10 min readWe tested 15 ML-KEM and ML-DSA implementations across 5 languages. Here's what we found — and what we didn't.
4 min readAn examination of Cryspen's 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 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 readTowards new queries, automated model translation and formalized semantics in Verifpal.
6 min readHow Verifpal sped up the formal modeling efforts for a new pandemic-tracing Protocol.
8 min read