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
hpke-ng: Faster, Smaller, Harder HPKE for Rust
Across 44 head-to-head benchmarks against hpke-rs, hpke-ng wins on 16 and ties the rest, ships a 30% smaller binary, 36% less project code, and a type system that catches four classes of bug at compile time.
Read →Announcing the Post-Quantum Migration Playbook
A 52-page practitioner guide for engineers and architects working on post-quantum migration, alongside an interactive scorecard and TLS scanner at pq-migration.symbolic.software.
Read →Verifpal 0.51.0: Sharper Semantics for Passwords, Assertions, and AEAD
Verifpal 0.51.0 tightens the analysis engine's treatment of password-qualified values, checked ASSERT? assertions, and AEAD associated data, all on the back of excellent bug reports from the community.
Read →
CEDARCRYPT 2026 · PAPHOS, CYPRUS
Summer school for applied cryptographers.
65
DAYS
UNTIL JULY 13
UNTIL JULY 13
The conference
ASummer school — workshops on PQC, secure messaging, formal verification3 days
BResearch conference — peer-reviewed talks1 day
▸CFP closes April 10, 2026submission
★Student scholarshipsPQShield + Zama
