Tools for design-level security.
Every piece of software we build started as a tool we needed for our own work—formal verification of protocols, conformance testing of post-quantum implementations, and privacy-preserving communications. All open source.
Secure Your Architecture
Our software
Magicall™: encrypted video calls without the surveillance
Magicall™ is our privacy-first video calling platform, built for people who believe their conversations shouldn't be training data. End-to-end encrypted with verifiable short authentication strings, browser-based with no downloads required, and featuring permanent room URLs that are always ready. Our newest launch!
- End-to-end encryption with AES-256-GCM, verified with short authentication strings (SAS).
- Zero downloads—works in Chrome, Firefox, Safari, Edge on desktop or mobile.
- Permanent room URLs: magicall.online/r/you, always ready to share.
- No ads, no AI training on your calls, no dark patterns. GDPR compliant and EU hosted.
Verifpal®: streamlining protocol verification
In a world where AI finds implementation bugs, the value of proving your protocol is correct by design becomes paramount. Verifpal® brings the power of symbolic formal verification to practitioners, students, and engineers who demand real-world applicability without losing the robustness of comprehensive verification features. Our flagship software!
- Intuitive language for modeling protocols that is straightforward to write and understand.
- Modeling language that reduces potential for new users to make mistakes in protocol definitions.
- Support for advanced security property queries, such as forward secrecy or key compromise impersonation.
- Ability to model protocols under an active attacker with unbounded sessions and fresh values.
Noise Explorer: formalizing Noise protocols
The Noise Protocol Framework is a design-level decision. Noise Explorer helps you make that decision with formal guarantees. Design Noise Handshake Patterns, generate formal verification models, browse a library of pre-computed verification results, and generate secure implementations in Go and Rust.
- User-friendly platform to design Noise Handshake Patterns.
- Library of pre-computed formal verification results for every standard pattern.
- Generates formal verification models.
- Generate reliable software implementations in Go, Rust and WebAssembly, ready for production use.
Kyber-K2SO: post-quantum primitives in Go
Post-quantum migration is a design-level decision that every cryptographic system will face. Kyber-K2SO is Symbolic Software's clean implementation of ML-KEM (FIPS 203), the standardized key encapsulation mechanism whose security is based on the hardness of solving the learning-with-errors (LWE) problem over module lattices.
- Clean Go reference implementation.
- High performance and ready for production use.
Crucible: conformance testing for post-quantum cryptography
Crucible is our open source conformance testing framework for ML-KEM (FIPS 203) and ML-DSA (FIPS 204) implementations. Born from real audit findings, it encodes the specific bug classes we've encountered — missing modulus checks, dead bounds checks, incorrect rounding — as targeted, reusable test batteries that any implementation can be wired up to.
- 129 tests across 12 categories targeting real-world bug classes from production audits.
- Tested against 15 implementations across Rust, Go, C, C++20, and Java.
- Simple JSON line protocol over stdin/stdout — wire up any implementation in minutes.
- Every test tagged with the bug class, FIPS spec section, and originating audit finding.
Ready to secure your architecture?
AI is changing what attackers can do. We help you change what they find.
Secure Your Architecture