Summer 2026 Research Internship at Symbolic Software
We're looking for a research intern to join us this summer and contribute to new papers on real-world cryptographic constructions.
3 min readFrom the lab.
Insights from our audit practice, software releases, and applied cryptography research. Updated whenever we publish.
CE Labs' Approach to TLS: A Critical Analysis
An examination of CE Labs' TLS implementations reveals 75% of valid ECDSA signatures rejected, authentication tags silently dropped, no certificate validation, and remote denial-of-service vectors.
11 min readMaking Verifpal Easier to Reason About
Verifpal's analysis engine has been redesigned with a unified equational theory, provenance-tagged values, a formally grounded deduction loop, and a bounded-depth search that runs 3x faster — plus updated tooling across the board.
11 min readVerifpal Workbench: Protocol Analysis in Your Browser
Verifpal now runs entirely in the browser via WebAssembly. The new Workbench at verifpal.com/workbench lets anyone write, verify, and visualize cryptographic protocol models with zero installation.
3 min readVerifpal, Rewritten in Rust
After seven years in Go, Verifpal has been completely rewritten in Rust, gaining a new analysis engine, massive performance improvements, a rich terminal interface, and a novel attack strategy that finds more attacks.
9 min readSecurity Announcement: Bugs in Noise Explorer's Rust/WASM Code Generation
We've updated Noise Explorer to address two bugs in generated Rust and WebAssembly implementations of Noise Protocol Framework handshake patterns.
2 min readEven More Bugs in CE Labs' libcrux: ML-DSA
Three findings in libcrux's ML-DSA implementation: a verifier norm check that is dead code due to a wrong constant, a missing bounds check in hint deserialization, and a wrong multiplication specification that renders AVX2 proofs unsound.
13 min readWe Found Bugs in CE Labs' Verified Code
CE Labs said they'd be 'very interested' if someone found a bug in their verified code. We found three.
12 min readVerifpal Verifies Signal Across Three Messages
Verifpal 0.31.2 ships a major overhaul to active attacker analysis, finally enabling full verification of Signal's three-message protocol.
7 min readOn the Promises of 'High-Assurance' Cryptography
A case study on CE Labs' libcrux exposing the gap between formal verification marketing and engineering reality.
10 min readAnnouncing Cedarcrypt: Applied Cryptography in the Mediterranean
We're thrilled to announce Cedarcrypt, a new applied cryptography summer school and conference.
2 min readKyber-K2SO 1.0: Now Implementing ML-KEM
Kyber-K2SO version 1.0 upgrades from Kyber v3 to ML-KEM, the NIST-standardized post-quantum key encapsulation mechanism.
4 min read