Software built by cryptographers.
At Symbolic Software, we build secure software that makes a difference—from privacy-first video calling to advanced research tools that contribute to peer-reviewed scientific publications. Our solutions are designed with cryptographic rigor, ensuring that your communications and protocols are secure and reliable.
Start a Project
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
Verifpal® is our innovative software solution for analyzing the security of cryptographic protocols. It's designed to bring 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
Noise Explorer is an online engine for reasoning about Noise Protocol Framework Handshake Patterns. Noise Explorer allows you to design Noise Handshake Patterns, generate formal verification models, explore a compendium of pre-computed formal verification results, and even generate secure software implementations in Go and Rust.
- User-friendly platform to design Noise Handshake Patterns.
- Explores a compendium of pre-computed formal verification results.
- Generates formal verification models.
- Generate reliable software implementations in Go, Rust and WebAssembly, ready for production use.
Kyber-K2SO: post-quantum primitives in Go
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. ML-KEM is based on the Kyber algorithm that was the winning candidate of the NIST post-quantum cryptography standardization project.
- Eminently readable Go reference implementation.
- High performance and ready for production use.
Want to work together?
Choose Symbolic Software as your trusted partner in enhancing security and fostering integrity within the digital ecosystem.
Start a Project