2026.08.15 · Software
Verifpal 1.0 removes the beta warning the tool has printed with every analysis since 2020, on the strength of a new paper. The language now covers post-quantum key exchange, declared weakening assumptions, witness-based unlinkability, and two concurrent sessions of every principal; the engine behind it comes with a soundness theorem that holds however the solver behaves, unconditional termination, and attack traces measured for readability against ProVerif and Tamarin.
20 min read
2026.08.08 · Software
Verifpal 0.80.0 lets a model declare that a particular piece of cryptography is broken (weak, forgeable, and from a chosen phase onward) instead of approximating the break with a list of leaked values, and decides unlinkability queries by searching for a concrete link witness that it then reports back to you.
19 min read
2026.08.05 · Software
Verifpal 0.70.0 removes Diffie-Hellman equations from the modelling language, adds a generic KEM for post-quantum and hybrid key exchange, rebuilds the active attacker around a search that works backwards from each query, and narrates every attack it finds as numbered causal steps.
20 min read
2026.04.20 · Software
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 read
2026.04.07 · Research
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 read
2026.03.07 · Research
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 read
2026.03.01 · Software
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
2026.02.24 · Software
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 read
2026.02.23 · Software
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 read
2026.02.17 · Research
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 read
2026.02.12 · Research
CE Labs said they'd be 'very interested' if someone found a bug in their verified code. We found three.
13 min read
2026.02.10 · Software
Verifpal 0.31.2 ships a major overhaul to active attacker analysis. Verifpal can now fully verify a model of Signal's three-message protocol, a result other tools reached years ago and that is new only for Verifpal.
7 min read
2026.02.05 · Research
A case study on CE Labs' libcrux exposing the gap between formal verification marketing and engineering reality.
10 min read
2020.09.02 · Software
Understanding Verifpal's relationship with cryptographic protocol security.
5 min read
2020.04.14 · Software
Towards new queries, automated model translation and formalized semantics in Verifpal.
6 min read
2020.04.05 · Software
How Verifpal sped up the formal modeling efforts for a new pandemic-tracing Protocol.
8 min read