# Symbolic Software

> Independent applied-cryptography consultancy. Design-level security for the AI era.

More than 300 design-level engagements.
Founded: 2017 · Paris, France. Representative: Dr. Nadim Kobeissi (nadim.computer).
Every engagement is led by a senior cryptographer. Scope, schedule, and fee agreed in writing before work begins.

Selected clients: 1Password, Bitwarden, Coinbase, Concordium, Dashlane, Digify, Ente, Ethereum Foundation, ExpressVPN, Linux Foundation, MetaMask, Mozilla, Native Labs, NordVPN, Taurus, Zoom.

Contact: business@symbolic.software.
The full corporate and legal record is at https://symbolic.software/about/.

## Practice

- [Security](https://symbolic.software/security/): review scope, deliverables, and public case studies.
- [Plan a review](https://symbolic.software/chat/): contact and scoping information. Calls at https://cal.com/symbolicsoft.
- [About](https://symbolic.software/about/): the practice, research, teaching, and company information.

- [You are designing or changing a protocol.](https://symbolic.software/security/#review-protocol): Threat modeling, protocol design, primitive selection, and formal analysis where useful.

- [You are preparing a product for release.](https://symbolic.software/security/#review-implementation): Cryptographic code, session state, and error handling in Go, Rust, TypeScript, Swift, Java, .NET, C, and Solidity.

- [You are planning a post-quantum migration.](https://symbolic.software/security/#review-post-quantum): KEM and signature choices, composition, conformance, and migration planning.

- [You need to assess a verification claim.](https://symbolic.software/security/#review-verification): Protocol models in Verifpal, ProVerif, or Tamarin, and review of verification coverage and toolchain boundaries.

## Public reports and technical analyses


- [CE Labs libcrux (2026)](https://symbolic.software/security/#case-celabs): We published five findings in libcrux and analyzed gaps between the code, Cryspen's hax verification pipeline, and the claims made for the library. The work is documented in two papers and an OSTIF talk.
  - [Read the series](https://symbolic.software/blog/2026-02-05-ce-labs/)
  - [Verification Theatre paper](https://eprint.iacr.org/2026/192)
  - [Verification Facade paper](https://eprint.iacr.org/2026/670)


- [Telegram MTProto (2026)](https://symbolic.software/security/#case-telegram): A technical review of Telegram's MTProto protocol under a network-attacker threat model, commissioned in 2025 by Global Network Solutions and made public in 2026 through a Swiss court filing. Conducted under editorial-independence terms reproduced verbatim in the report.
  - [View report](https://symbolic.software/pdf/gnmx-01.pdf)
  - [Read the post](https://symbolic.software/blog/2026-05-21-telegram-mtproto-review/)


- [dWallet Labs (2024)](https://symbolic.software/security/#case-dwallet): With 3MI Labs, we compared dWallet Labs' Rust implementation with the 2PC-MPC protocol and reviewed the supporting crates. The report records three security findings, including critical nonce reuse in the decentralized-party presigning step.
  - [View report](https://symbolic.software/pdf/dw-01.pdf)


- [Native Labs (2023)](https://symbolic.software/security/#case-nativelabs): We reviewed the Native Labs smart contracts, including gas use, interoperability, transaction flows, liquidity models, code quality, and their effects on the user experience.
  - [View report](https://symbolic.software/pdf/nat-001.pdf)


- [1Password (Multiple engagements)](https://symbolic.software/security/#case-onepassword): This work with Cure53 covered key rotation, vault security under server compromise, and public-key validation in 1Password B5.
  - [View report](https://symbolic.software/pdf/pentest-report_1password-b5.pdf)


- [Mozilla Thunderbird Enigmail (2017)](https://symbolic.software/security/#case-thunderbird): In our first client engagement, we worked with Cure53 on Mozilla Thunderbird's Enigmail PGP integration and identified a critical flaw in the signature path.
  - [View report](https://symbolic.software/pdf/pentest-report_thunderbird-enigmail.pdf)

## Open source

[Software](https://symbolic.software/software/) describes the tools and their intended uses.


### 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

Limitations: 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.
- [verifpal.com](https://verifpal.com)
- [github](https://github.com/symbolicsoft/verifpal)


### 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
- [github](https://github.com/symbolicsoft/crucible)
- [blog post](https://symbolic.software/blog/2026-03-23-crucible/)


### 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
- [github](https://github.com/symbolicsoft/hpke-ng)


### 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
- [github](https://github.com/symbolicsoft/kyber-k2so)
- [release notes](https://symbolic.software/blog/2025-12-21-kyberk2so10/)


### 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
- [download the playbook (PDF)](https://pq-migration.symbolic.software/static/pdf/playbook.pdf)
- [try the scanner](https://pq-migration.symbolic.software)


### 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
- [paper (eprint 2026/1103)](https://eprint.iacr.org/2026/1103)
- [github](https://github.com/symbolicsoft/jevil)
- [blog post](https://symbolic.software/blog/2026-05-31-jevil/)


### Noise Explorer

Design Noise Handshake Patterns, inspect pre-computed verification results, and generate implementations in Go, Rust, and WebAssembly.
[noiseexplorer.com](https://noiseexplorer.com)

## Research

- Verification coverage: Two papers on defects in libcrux and the structural gaps in its verification pipeline.
  - [Verification Theatre](https://eprint.iacr.org/2026/192)
  - [Verification Facade](https://eprint.iacr.org/2026/670)

- Protocol verification: The soundness, termination, trace readability, and limitations of Verifpal.
  - [Verifpal Seven Years Later](https://eprint.iacr.org/2026/1654)

- Machine-checked security bounds: An Ethereum Foundation-proposed Lean 4 restatement of soundcalc, developed by our Summer 2026 research interns.
  - [soundcalc-lean](https://github.com/symbolicsoft/soundcalc-lean)
  - [Meet the summer team](https://symbolic.software/blog/2026-07-29-summer-team/)

## Positions

- [Recommending post-quantum native design under epistemic duress](https://symbolic.software/blog/2026-04-02-pq-native/): we recommend all new cryptographic systems be designed post-quantum native. The recommendation is deliberately hedged; the caveats are part of it.
- [Hybrid constructions are a safety blanket, and that's fine](https://symbolic.software/blog/2026-04-13-hybrid-constructions/): hybrid KEMs yes, hybrid signatures usually no.
- [On the promises of "high-assurance" cryptography](https://symbolic.software/blog/2026-02-05-ce-labs/): what a formal-verification claim does and does not buy you.
- [Verifpal reaches 1.0](https://symbolic.software/blog/2026-08-15-verifpal-1-0/): what the tool now claims, and what it deliberately does not.

## Teaching

- [Applied Cryptography](https://symbolic.software/course/): a university course with public slides, readings, problem sets, projects, and lecture recordings. Course site: https://appliedcryptography.page
- [Summer 2026 cohort](https://symbolic.software/blog/2026-05-12-course-summer-2026/): the admitted students and the summer program.
- [Cedarcrypt](https://cedarcrypt.org): applied-cryptography summer school and research conference run with the IACR at AUB Mediterraneo in Paphos, Cyprus.
- [Why I teach cryptography in Lebanon](https://symbolic.software/blog/2026-07-22-why-i-teach-cryptography-in-lebanon/): the reasoning behind the teaching program.

## More

- [Blog](https://symbolic.software/blog/): audit findings, advisories, releases, and research. [RSS](https://symbolic.software/index.xml).
- [Security posts](https://symbolic.software/categories/security/) and [research posts](https://symbolic.software/categories/research/).
- [Sitemap](https://symbolic.software/sitemap.xml).