Magicall™
Privacy-first video calling: AES-256-GCM end-to-end with verifiable short authentication strings, browser-based with no installs, permanent room URLs, and zero ads or AI training.
magicall.online →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, encrypted video calling. All open source, most cited in the literature, all production-deployed somewhere we can name and somewhere we can't.
toolversionsummary
verifpal
v0.51
✓
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
⊕ 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, post-quantum primitives, and more — under an active attacker, with unbounded sessions and fresh values. Used in production audits and taught in cryptography courses worldwide.
- 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.
- 129 ML-KEM tests + 87 ML-DSA tests across 12 categories
- Tested against 15 implementations across Rust, Go, C, C++20, Java
- JSON-line protocol over stdin/stdout — wire any implementation in minutes
- Every test traces back to a real audit finding
[cat 01]keygen12/12 ✓
[cat 02]sign14/14 ✓
[cat 03]verify11/11 ✓
[cat 04]ntt-bounds8/8 ✓
[cat 05]rejection-sampling7/7 ✓
[cat 06]hint-overflow5/5 ✓
✓87/87 pass · 9 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, zero-dep aside from RustCrypto, designed to be both auditable and maximally 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 = 1184 B (PQ hybrid · classical fallback if either KEM falls)
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_std friendly
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, what the library landscape looks like 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
Also from us
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 →Built for our own audit work, released for everyone.
Repos
All seven tools live on GitHub. Issues open to the public; PRs reviewed within the week.
github.com/symbolicsoft →Discuss
Cryptographic protocol questions, bug reports, feature requests — Discord is the fastest path.
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 that cannot afford to get cryptography wrong.
Secure your architecture →