12 posts in category “Software”.
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 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 readWe tested 15 ML-KEM and ML-DSA implementations across 5 languages. Here's what we found — and what we didn't.
4 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 readAfter 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 0.31.2 ships a major overhaul to active attacker analysis, finally enabling full verification of Signal's three-message protocol.
7 min readWe're launching Magicall, a privacy-first video calling platform built by cryptographers.
7 min readKyber-K2SO version 1.0 upgrades from Kyber v3 to ML-KEM, the NIST-standardized post-quantum key encapsulation mechanism.
4 min readUnderstanding Verifpal's relationship with cryptographic protocol security.
5 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