Design-level security
for the AI era.
An applied cryptography practice. We audit at the layer above implementation — protocol architecture, primitive selection, threat modeling, formal verification — where AI bug-finders cannot help and humans still must.
attacker[active]
principal Alice[
knows public c0
generates a
ga = G^a
]
Alice → Bob: ga
principal Bob[
knows public c0
generates m1, b
gb = G^b
gab = ga^b
e1 = AEAD_ENC(gab, m1, c0)
]
Bob → Alice: gb, e1
protocol diagram
2 actors · 2 messages
queries — security goals
✗
confidentiality?
m1
ATTACK FOUND
✗
authentication?
Bob → Alice: e1
ATTACK FOUND
Our practice areas
01 / SECURITY
Audits
Protocol architecture, cryptographic review, threat modeling, formal verification.
○ Mozilla · 1Password · Coinbase
○ Zoom · Bitwarden · MetaMask
250+ engagements →
02 / SOFTWARE
Tools
Verifpal, Crucible, hpke-ng, Kyber-K2SO, PQ Migration Playbook.
$ verifpal verify tls13.vp
→ ✓ verified · 0.34s
open source →
03 / COURSE
Teaching
Applied Cryptography. Free for 50 Lebanese students this summer.
∫ provable security
⊕ TLS · ZK · PQC · MPC
2026 cohort open →
04 / RESEARCH
Lab
Post-Quantum Migration Playbook, advisories, papers, the audit floor.
PQ Playbook3247×
Advisories shipped12
new: PQ Playbook →
From the audit floor
Bug classes we keep finding. Anonymized; representative; the kind of thing AI bug-finders catch after we have already shipped a fix.
Constant-time leak in ECC point doubling
AEAD nonce reuse under concurrent state
Incorrect rounding in lattice solver
Public key not validated to correct subgroup
Unchecked length field in TLV parser
Crucible.
Bug classes,
encoded as tests.
129 tests across 12 categories, each tagged with the bug class, the FIPS spec section, and the audit it came from. Wire any ML-KEM or ML-DSA implementation up over stdin/stdout. Pass or fail in seconds.
129tests
12categories
15implementations tested
5languages supported
tests passed
127 / 129
98.4% pass
2 fail
key generation12/12
encapsulation14/14
decapsulation11/11
NTT bounds7/8
rejection sampling9/9
serialization14/14
decompression5/6
hash domain sep8/8
parameter hygiene11/11
From the lab
On Our Telegram MTProto Review
A note on Symbolic Software's technical review of Telegram's MTProto protocol, made public in 2026 through litigation. Covers the auth_key_id tracking vulnerability, the empirical case against Telegram's 'changes regularly' rebuttal, the editorial independence terms of the engagement, and how the document entered the public record.
Read →Applied Cryptography Course: Welcome, Class of Summer 2026!
Fifty students from nine institutions have been selected for the Summer 2026 Applied Cryptography online program, our free intensive course bringing modern cryptography to Lebanese university students. Here's a quick look at what the course covers, and at the wonderful group joining us this June.
Read →hpke-ng: Faster, Smaller, Harder HPKE for Rust
126 head-to-head benchmarks against hpke-rs and rust-hpke. hpke-ng wins 103, ties 19, loses 4. ML-KEM-1024 decap −55%, X25519 decap −41%, export −72% to −76%, end-to-end roundtrip −30% — and a type system that catches four classes of bug at compile time.
Read →The program
1Welcome & FoundationsMon, Jul 13
2Applied Cryptography in PracticeTue, Jul 14
3Protocols & PrimitivesWed, Jul 15
4Advanced Constructions & ClosingThu, Jul 16
