Insights from our audit practice, software releases, and applied cryptography research. Updated whenever we publish.
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.
4 min readCedarcrypt'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.
12 min readA 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.
11 min readA 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.
13 min readFifty 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.
4 min read126 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.
27 min readA 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.
1 min readVerifpal 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.
7 min readWhy Symbolic Software agrees with Soatok's position on hybrid post-quantum constructions: hybrids are compelling for KEMs, far less necessary for signatures, and the real risk is migration friction.
6 min readFive proof-of-concept exploits against ML-DSA, ML-KEM, Ed25519, and ChaCha20 demonstrate three classes of semantic gap in hax's Rust-to-F* extraction pipeline, where verified models diverge from deployed code.
11 min readSymbolic Software is recommending post-quantum native design for all new cryptographic systems. This post examines the evidence behind that recommendation, its limitations, and the epistemic questions the industry should be confronting.
10 min readWe're opening 50 spots for students at Lebanese universities to take the Applied Cryptography course online, completely free of charge, starting June 2026. Applications are open now.
3 min read