Applied Cryptography: Summer 2026 Cohort
Fifty students from nine institutions were admitted to the free Summer 2026 Applied Cryptography online course.
2 min readWriting.
Audit reports, security advisories, software releases, research, and essays.
hpke-ng: Faster, Smaller, Harder HPKE for Rust
126 head-to-head benchmarks against hpke-rs and rust-hpke. hpke-ng wins 103, ties 19, loses 4. ML-KEM-1024 decap −55%, X25519 decap −41%, export −72% to −76%, end-to-end roundtrip −30%, plus a type system that catches four classes of bug at compile time.
26 min readAnnouncing the Post-Quantum Migration Playbook
A 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: Sharper Semantics for Passwords, Assertions, and AEAD
Verifpal 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 readHybrid Constructions Are a Safety Blanket, and That's Fine
Why 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 readThe Verification Facade: Structural Gaps in Cryspen's Hax Pipeline
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 readRecommending Post-Quantum Native Design Under Epistemic Duress
Symbolic 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 readApplied Cryptography: Free Online Course for 50 Lebanese University Students This Summer
We'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 readCrucible: Forging Post-Quantum Implementations in the Fire of Real Audit Findings
We tested 15 ML-KEM and ML-DSA implementations across 5 languages, and found two conformance gaps and no security vulnerabilities.
4 min readSummer 2026 Research Internship at Symbolic Software
We're looking for a research intern to join us this summer and contribute to new papers on real-world cryptographic constructions.
3 min readCE Labs' Approach to TLS: A Critical Analysis
An 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 readMaking Verifpal Easier to Reason About
Verifpal'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 read