Noise Explorer
A platform for designing Noise Handshake Patterns, browsing pre-computed verification results for every standard pattern, and generating implementations in Go, Rust, and WebAssembly.
noiseexplorer.com →Tools for design-level
security.
Every tool we build started as something we needed for our own audit work: formal verification, post-quantum conformance testing, hybrid KEM implementations. All of them are open source and deployed in production, and most are cited in the literature.
toolversionsummary
verifpal
v1.0
✓
protocol verification
crucible
v1.0
✓
PQ conformance testing
hpke-ng
v0.1.0
✓
RFC 9180 (classical + PQ)
kyber-k2so
v1.0
✓
ML-KEM in Go
pq-playbook
2026-Q2
✓
migration guide + scanner
jevil
v0.1.0
✓
few-time signatures
⊕ open source · MIT & Apache 2.0 · github.com/symbolicsoft
Verifpal: protocol verification, in your language
Verifpal brings symbolic protocol verification to practitioners. Model Diffie–Hellman, signatures, AEAD, and post-quantum primitives under an active attacker, with unbounded sessions and fresh values. We use it in our own audits, and it is taught in university cryptography courses.
- Intuitive language, easier than ProVerif or Tamarin for first-time modelers
- Pre-computed verification of forward secrecy, key compromise impersonation, and post-compromise security
- Browser-based Workbench with no install
attacker[active]
principal Alice[ generates s_a, e_a ]
principal Bob[ generates s_b, e_b ]
Alice → Bob: e
Bob → Alice: e, ee, s, es
Alice → Bob: s, se, ENC(K, m)
✓3/3 queries pass · 0.27s · forward secrecy
Crucible: bug classes, encoded as tests
Crucible exercises post-quantum implementations against the bug classes we keep finding in production audits. Each test is tagged with the bug class, the FIPS spec section, and the originating audit finding. Wire any ML-KEM or ML-DSA implementation up over stdin/stdout.
- 78 ML-KEM tests + 51 ML-DSA tests across 12 categories
- Tested against 19 implementations across Rust, Go, C, C++20, Java, JavaScript, and Zig
- JSON-line protocol over stdin/stdout, so wiring up an implementation takes minutes
- Every test traces back to an audit finding
[cat 01]norm-checks9/9 ✓
[cat 02]arithmetic9/9 ✓
[cat 03]signing9/9 ✓
[cat 04]verification9/9 ✓
[cat 05]serialization9/9 ✓
[cat 06]timing6/6 ✓
✓51/51 pass · 6 categories · conformant
hpke-ng: RFC 9180, classical and post-quantum
A clean-slate Rust implementation of HPKE (RFC 9180), with first-class support for hybrid post-quantum KEMs via X-Wing (ML-KEM-768 ⊕ X25519). no_std friendly, with no dependencies beyond RustCrypto. Built to be auditable and fast.
- Classical KEMs: X25519, X448, P-256/384/521, secp256k1
- Post-quantum KEMs: ML-KEM, X-Wing (hybrid)
- AEADs: AES-128/256-GCM, ChaCha20-Poly1305
- Differential and conformance testing built in
// sender
let(enc, ct) = Seal(pkR, info, aad, msg)
└─ kem = X25519 ⊕ ML-KEM-768
└─ aead = ChaCha20-Poly1305
// recipient
letmsg = Open(skR, enc, ct, info, aad)
✓decapsulated · 0.18ms
ct = 1120 B (PQ hybrid · secure while either KEM holds)
Kyber-K2SO: ML-KEM in Go, no surprises
A clean reference implementation of ML-KEM (FIPS 203) in pure Go. Suitable for production deployment where post-quantum key encapsulation is needed without pulling in C dependencies.
- FIPS 203 conformant (verified by Crucible)
- ML-KEM-512, -768, -1024 supported
- Pure Go, no C dependencies
KeyGenpk = 1184 B sk = 2400 B
Encapsct = 1088 B ss = 32 B
Decapsss′ = ss✓
bench (M2 Pro):
keygen 0.04ms · encap 0.05ms · decap 0.06ms
FIPS 203 · pure Go · no C dependencies
PQ Migration Playbook: everything we tell clients
A 52-page practitioner's guide to post-quantum migration: which primitive to choose, when to hybridize and when to stop, how to migrate TLS without breaking production, which libraries are usable today. Companion scorecard and TLS scanner.
- Ten chapters from primitives through rollout strategy
- Audit-floor bug classes documented anonymized
- Free, no signup, no email gate
- Companion scorecard scores your stack across 6 dimensions in 3 minutes
TLS endpoints▓▓▓▓▓▓▓▓▓▓100%
PKI signatures▓▓▓▓▓▓▓▓░░82%
KEM hybridization▓▓▓▓▓▓░░░░60%
Library inventory▓▓▓▓▓▓▓▓▓░90%
Conformance suite▓▓▓▓▓░░░░░50%
Rollout strategy▓▓▓▓▓▓▓▓▓▓100%
↳ playbook.pdf · 52 pages · 3,247 downloads
Jevil: catastrophic failure, by design
A post-quantum, transparent few-time signature scheme with a sharp key-recovery cliff: signatures one through n* are unforgeable; the (n*+1)-th makes the entire secret polynomial publicly recoverable. The cap is enforced by the algebra of a committed polynomial, not by a counter.
- First post-quantum and transparent FTS with a sharp cliff, not a soft slope
- 68-byte public keys, 32-byte secret keys, ~40 KB to ~500 KB signatures
- Built on zk-WHIR polynomial commitments: no trusted setup, no Shor break
- Over-signing is self-punishing: the key becomes public in O(D²)
// sign 7 messages, each reveals K points of f
sign(m₁) … sign(m₇) ✓
└─ distinct evals = 14 / 16 · f still hidden
// the 8th signature, one past the budget
sign(m₈)
└─ distinct evals = 16 / 16
f recovered · Lagrange in O(D²), the key is public.
Also from us
Tools we built for our own audit work.
Repos
Eight open-source projects, from Verifpal to Jevil. Issues open to the public; PRs reviewed within the week.
github.com/symbolicsoft →Discuss
Discord is the fastest path for cryptographic protocol questions, bug reports, and feature requests.
discord →Want us to audit your cryptography?
Open source tools are a fraction of what we do. Most of our work is design-level audit engagements for organizations shipping cryptography to production.
Secure your architecture →