Security Research & Advanced Cryptography
zk.golf is a platform where people can compete on creating the most efficient zk circuits for specific problems. It is enabled by what we call "fearless optimization", which is achieved by combining formal verification and frontier AI models. By the end, you will be convinced that nobody should look at constraints ever again in their life.
Read →
A month after launching mpcsec.org, we added a searchable tracker of real-world MPC bugs, expanded the pitfall taxonomy, published contribution templates and refreshed the site UI.
Read →zkNews is now open to everyone. When we first launched, access was limited to a small beta group to keep things stable while we found our footing. That rate limit is gone. Anyone can now sign up, submit links, and join the discussion at news.zksecurity.xyz. Come help us build the home for zero-knowledge news.
Read →
Clean, our circuit DSL, is growing toward verification of complex multi-AIR ensembles. We introduce channels as a way to model lookups, permutation arguments, and zkVM cross-table interactions, then explain how local gadget proofs can compose into global soundness theorems. Watch our talk from ZKProof 8 or read the post.
Read →
mpcsec.org is a new collaborative reference for common pitfalls in MPC implementations and the cryptographic primitives they rely on, built with contributors from zkSecurity, Trail of Bits, Partisia, and Zama. If you build, audit, or deploy threshold signatures, distributed key generation, or other MPC protocols, it's a starting point for the mistakes you don't want to repeat.
Read →This post is all about the maps that let us move between modules without breaking their structure. We’ll see when a map is truly “linear,” when two modules are (secretly) the same, and why two-input maps deserve special attention. Along the way, (bi-)linear maps and isomorphisms become less like abstract definitions and more like tools we can actually use. By the end, we’ll have all the tooling we need to tackle abstract tensor products head-on.
Read →In this part of our series, we start introducing the algebraic language needed to formalize sum-check as a tensor reduction. We start with the basics of rings and modules. Rings generalize fields by dropping the requirement that every non-zero element has a multiplicative inverse. Modules then generalize vector spaces by allowing scalars to come from a ring instead of a field. In this post, we’ll use plenty of examples to make these ideas concrete and build intuition along the way.
Read →We found a critical soundness bug in Jolt’s transparent verifier that allowed a forged proof for an invalid execution to verify. The issue was fixed quickly after disclosure, and the full PoC and write-up are available in the linked repository.
Read →
Notes and proofs for the divisor-based ECIP protocol of Eagen, written with Diego F. Aranha and supported by MAGIC Grants. The document is self-contained: it works through the necessary algebraic geometry, the interactive proof and its soundness, the composition with a simulation-extractable NIZK, and the R1CS verifier circuit used by Parker's gadget in Monero's FCMP++.
Read →Encrypted mempools are an emerging approach to reducing transaction-ordering MEV. They are not just normal mempools with encryption added on top: they introduce a new security boundary around the exact moment a transaction becomes plaintext. This post explains the security model, the core invariant, and the subtle failure modes protocol designers need to consider.
Read →
On May 7th, we'll be in Rome sponsoring zkSummit14. A look back at a decade of progress in zero-knowledge, the current state of ZK security based on 100+ audits, and why events like zkSummit have become infrastructure for the field.
Read →
A one-character repeated-squaring bug in Inferno's Limbo implementation turns the intended random polynomial check into a linearized Frobenius check over a binary extension field. This post walks through why the usual Schwartz-Zippel argument disappears, how periodicity of the Frobenius map makes collisions immediate after 64 multiplication gates, and how even smaller circuits can cheat with noticeably higher probability.
Read →We walk through a Lean 4 proof of correctness for a Clean model of circomlib's optimized Poseidon hash circuit at arity 1. The theorem says the modeled constraints are sound and complete with respect to the optimized Poseidon spec. After weeks of work, the only remaining `sorry` was a primality proof for the BN254 scalar field: a 254-bit number that no proof assistant can decide by trial division. Closing it requires a Pratt certificate, a recursive proof structure based on a theorem Lucas published in 1876.
Read →
Groth16 is still the gold standard for succinct SNARKs: 128-byte proofs, constant-size verification, and a decade of real-world deployment. But despite its ubiquity, almost nobody explains *why* it works the way it does. In this post, we build Groth16 from the ground up, starting from R1CS and QAPs, then layer in pairings, trusted setup parameters, and the separator tricks (α, β, γ, δ) that make the scheme sound. By the end, you should have an intuitive grasp of every term in the final verifier equation.
Read →