Design-level security
for the AI era.

An applied cryptography practice. We audit the layer above implementation: protocol architecture, primitive selection, threat modeling, formal verification. AI bug-finders do not work at that layer.

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
alice bob ga gb, e1
queries — security goals
✗ confidentiality? m1 ATTACK FOUND
✗ authentication? Bob → Alice: e1 ATTACK FOUND
✗ 2 of 2 queries failed · 0.21s Verifpal v0.70
Latest 2026.08.15 Verifpal Reaches 1.0: A Toy Becomes an Instrument 2026.08.08 Verifpal 0.80.0: Nuancing Weak Cryptography Modeling and Witness-Based Unlinkability 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

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, with client details removed.

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 and get a 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.15 · Software

Verifpal Reaches 1.0: A Toy Becomes an Instrument

Verifpal 1.0 removes the beta warning the tool has printed with every analysis since 2020, on the strength of a new paper. The language now covers post-quantum key exchange, declared weakening assumptions, witness-based unlinkability, and two concurrent sessions of every principal; the engine behind it comes with a soundness theorem that holds however the solver behaves, unconditional termination, and attack traces measured for readability against ProVerif and Tamarin.

Read →
2026.08.08 · Software

Verifpal 0.80.0: Nuancing Weak Cryptography Modeling and Witness-Based Unlinkability

Verifpal 0.80.0 lets a model declare that a particular piece of cryptography is broken (weak, forgeable, and from a chosen phase onward) instead of approximating the break with a list of leaked values, and decides unlinkability queries by searching for a concrete link witness that it then reports back to you.

Read →
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 →

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 →