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 readSoftware
13 posts in category “Software”.
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% — and a type system that catches four classes of bug at compile time.
26 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 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 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 readVerifpal, Rewritten in Rust
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 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 readIntroducing Magicall: Encrypted video calls that actually work
We're launching Magicall, a privacy-first video calling platform built by cryptographers.
7 min readKyber-K2SO 1.0: Now Implementing ML-KEM
Kyber-K2SO version 1.0 upgrades from Kyber v3 to ML-KEM, the NIST-standardized post-quantum key encapsulation mechanism.
4 min readOne Year of Verifpal
Understanding Verifpal's relationship with cryptographic protocol security.
5 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