Noise Explorer
Design Noise Handshake Patterns, inspect pre-computed verification results, and generate implementations in Go, Rust, and WebAssembly.
noiseexplorer.com →Open-source
cryptography.
We maintain tools for protocol verification, post-quantum conformance testing, HPKE, ML-KEM, and post-quantum migration. Source code and issue trackers are public.
Verifpal: symbolic protocol verification
Verifpal models cryptographic protocols under an active or passive attacker. It supports Diffie–Hellman, signatures, authenticated encryption, post-quantum KEMs, and compromise scenarios.
- A small modeling language for principals, messages, primitives, and security queries
- Queries for confidentiality, authentication, freshness, unlinkability, and compromise scenarios
- Browser-based Workbench
Scope of the result. A reported attack is real under the model's assumptions. A Pass means no attack was found within the bounded session count; it is not a proof of security. Sessions are bounded, and the tool does not support observational equivalence or user-defined equational theories.
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 · bounded sessions
Crucible: ML-KEM and ML-DSA conformance tests
Crucible tests ML-KEM and ML-DSA implementations against FIPS 203 and FIPS 204. Implementations connect to the runner through a JSON Lines interface over standard input and output.
- 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
- Each test cites the relevant FIPS section
- Tests prompted by audit findings include a reference to the 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: HPKE in Rust
A Rust implementation of HPKE (RFC 9180), including X-Wing support for hybrid post-quantum key exchange. It supports no_std and uses RustCrypto dependencies.
- 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
A pure-Go implementation of ML-KEM (FIPS 203), with support for ML-KEM-512, ML-KEM-768, and ML-KEM-1024.
- Passes the Crucible FIPS 203 test suite
- 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
Post-Quantum Migration Playbook
A practitioner guide to primitive selection, hybrid constructions, TLS and PKI migration, libraries, conformance testing, and rollout planning. The site also includes a readiness scorecard and TLS scanner.
- Ten chapters covering design choices and deployment
- Anonymized implementation problems observed during audits
- PDF available without registration
- Companion readiness scorecard and TLS scanner
[01]primitives and security levels
[02]hybrid KEMs and signatures
[03]TLS and PKI migration
[04]secure messaging
[05]libraries and conformance testing
[06]rollout planning
10 chapters · readiness scorecard · TLS scanner
Jevil: few-time signatures with a key-recovery threshold
A post-quantum, transparent few-time signature scheme. Signing beyond the configured budget makes the secret polynomial recoverable; the limit is enforced by the committed polynomial rather than a stateful counter.
- Post-quantum and transparent, with no trusted setup
- 68-byte public keys, 32-byte secret keys, ~40 KB to ~500 KB signatures
- Uses zk-WHIR polynomial commitments
- The secret becomes recoverable in O(D²) after the signing budget is exceeded
// 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.
Other software
Open-source projects.
Code
Browse the source, releases, issue trackers, and contribution guidelines on GitHub.
github.com/symbolicsoft →Support
Use each project's issue tracker for bugs and feature requests, or join the community Discord.
discord →Review the system around the primitives.
Primitive conformance and protocol analysis answer specific questions. We also review your threat model, key management, composition, and implementation together.
Explore review scope →