How Jevil works
A playground-first, interactive explainer for Jevil, a post-quantum, transparent few-time signature scheme whose key-recovery threshold is a single sharp cliff rather than a slow slope.
11 min readResearch
18 posts in category “Research”.
On Our Telegram MTProto Review
A note on Symbolic Software's technical review of Telegram's MTProto protocol, made public in 2026 through litigation. Covers the auth_key_id tracking vulnerability, the empirical case against Telegram's 'changes regularly' rebuttal, the editorial independence terms of the engagement, and how the document entered the public record.
13 min readhpke-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% — and 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.
10 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. Here's what we found — and what we didn't.
4 min readCryspen's Approach to TLS: A Critical Analysis
An 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 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 readVerifpal Workbench: Protocol Analysis in Your Browser
Verifpal 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 readEven More Bugs in Cryspen's libcrux: ML-DSA
Three 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 readWe Found Bugs in Cryspen's Verified Code
Cryspen said they'd be 'very interested' if someone found a bug in their verified code. We found three.
12 min readVerifpal Verifies Signal Across Three Messages
Verifpal 0.31.2 ships a major overhaul to active attacker analysis, finally enabling full verification of Signal's three-message protocol.
7 min readOn the Promises of 'High-Assurance' Cryptography
A case study on Cryspen's libcrux exposing the gap between formal verification marketing and engineering reality.
10 min readBetter Queries for Verifpal
Towards new queries, automated model translation and formalized semantics in Verifpal.
6 min readModeling DP-3T With Verifpal
How Verifpal sped up the formal modeling efforts for a new pandemic-tracing Protocol.
8 min read