Insights from our audit practice, software releases, and applied cryptography research. Updated whenever we publish.
Across 62 head-to-head benchmarks against hpke-rs, hpke-ng wins 27 — including ML-KEM decap at 54–55% faster and the entire post-quantum encap/decap path with no PQ losses — ties 32, ships a 30% smaller binary, and a type system that catches four classes of bug at compile time.
19 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 read