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.

Secure your architecture → See our work

verifpal · simple.vp

Attack found

attacker[active]
 
principal Alice[
  knows public c0
  generates a
  ga = PUBKEY(a)
]
Alice → Bob: ga
 
principal Bob[
  knows public c0
  generates m1, b
  gb = PUBKEY(b)
  gab = DH_KEX(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

Latest 2026.08.05 Verifpal 0.70.0: Post-Quantum Key Exchange, and an Attacker That Works Backwards 2026.07.29 Meet the Symbolic Software Summer 2026 Team 2026.07.22 Why I Teach Cryptography in Lebanon 2026.05.31 How Jevil works

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.

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 →

Trusted by

From the audit floor

Recurring bug classes from our audit work, anonymized.

Bug class · Cryptographic implementation

r = ntt_inv(c)

// ✗ no r < q check

Missing modulus check, NTT inverse

Found in 3 audits 5 codebases

Bug class · Side channels

if (secret_bit) {

ec_double(P)// timing

}

Constant-time leak in ECC point doubling

Found in 2 audits Wallet · VPN

Bug class · Protocol composition

nonce ← counter++

// race: two senders,

// same n → ENC reuse

AEAD nonce reuse under concurrent state

Found in 4 audits 2 messengers

Bug class · PQ rounding

q_half = (q + 1) >> 1

// ⌊⌋ used, ⌈⌉ needed

Incorrect rounding in lattice solver

Found in 2 audits ML-KEM impls

Bug class · Validation

K = a · peer_pk

// missing:

// peer_pk ∉ 𝒢′

Public key not validated to correct subgroup

Found in 3 audits 2 wallets

Bug class · Parsing

len = read_u32(buf)

read(buf, len)⚠

// len is hostile

Unchecked length field in TLV parser

Found in 5 audits 3 protocols

Conformance testing

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

View on GitHub →

crucible · ml-kem+ml-dsa.run

Running

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

Recent writing All posts →

2026.08.05 · Software

Verifpal 0.70.0: Post-Quantum Key Exchange, and an Attacker That Works Backwards

Verifpal 0.70.0 removes Diffie-Hellman equations from the modelling language, adds a generic KEM for post-quantum and hybrid key exchange, rebuilds the active attacker around a search that works backwards from each query, and narrates every attack it finds as numbered causal steps.

Read →

2026.07.29 · Announcement

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 →

2026.07.22 · Essay

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 →

The program

July 13–16, 2026 Paphos, Cyprus AUB Mediterraneo

1Welcome & FoundationsMon, Jul 13

2Applied Cryptography in PracticeTue, Jul 14

3Protocols & PrimitivesWed, Jul 15

4Advanced Constructions & ClosingThu, Jul 16

View full program at cedarcrypt.org →

Design-level security
for the AI era.