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
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
SECURE
✓
authentication?
Bob → Alice: e1
SECURE
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
Security has to start at the design level.
Protocol architecture, primitive selection, threat modeling, formal verification — everything downstream is a consequence of those decisions. More than 250 engagements since 2017 have started from that premise.
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 in session →
04 / RESEARCH
Lab
Post-Quantum Migration Playbook, advisories, papers, the audit floor.
PQ Playbook3247×
Advisories shipped12
new: PQ Playbook →
From the audit floor
Recurring bug classes from our audit work, anonymized.
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
19implementations tested
7languages supported
tests passed
127 / 129
98.4% pass
2 fail
kem/compression12/12
kem/ntt21/21
kem/bounds8/9
kem/decapsulation12/12
kem/serialization12/12
kem/sampling12/12
dsa/norm-checks9/9
dsa/arithmetic9/9
dsa/signing9/9
dsa/verification9/9
dsa/serialization8/9
dsa/timing6/6
From the lab
Meet the Symbolic Software Summer 2026 Team
Five people joined us this summer: two research interns formalizing zkVM soundness bounds in Lean, and three teaching assistants running the Applied Cryptography course. Here they are, in their own words.
Read →Why I Teach Cryptography in Lebanon
Cedarcrypt's first edition has concluded. On what a year of teaching cryptography in and for Lebanon has meant, why the conference met in Cyprus rather than Beirut, and the decades of work ahead.
Read →How Jevil works
A playground-first, interactive explainer for Jevil, a post-quantum, transparent few-time signature scheme whose key-recovery threshold is a single sharp cliff rather than a slow slope.
Read →The program
1Welcome & FoundationsMon, Jul 13
2Applied Cryptography in PracticeTue, Jul 14
3Protocols & PrimitivesWed, Jul 15
4Advanced Constructions & ClosingThu, Jul 16