ZK Circuits are a core component of integrating ZK proofs into real world applications, enabling the proving of arbitrary NP complete statements privately. A 2024 analysis revealed that approximately 96% of documented bugs in SNARK-based ZK systems were caused by under-constrained circuits, which are circuits that lack sufficient checks to prevent invalid proofs from passing verification. These vulnerabilities have enabled everything from unlimited token counterfeiting (Zcash, 2018) to $1.9 billion in forged withdrawals (zkSync Era, 2023). Thus, it is necessary to understand the security considerations when writing and designing circuits for usage in protocols and applications.
https://www.nethermind.io/blog/zk-circuit-security-a-guide-for-engineers-and-architects
This post compares the size of signatures and aggregates for transactions using Falcon signatures (as defined in the Falcon specification), under different assumptions about key recovery and aggregation.
https://ethresear.ch/t/revisiting-falcon-signature-aggregation-for-pq-mempools/24431
Industry broadly shipped PQ key exchange first (Chrome, iMessage, AWS, Cloudflare); PQ authentication is still early, especially in default public-web PKI. Ethereum inherits PQ transport encryption for some surfaces (HTTPS/JSON-RPC over TLS via Go 1.24), but application-layer privacy — cryptographic protocols built on top of the EVM rather than natively supported by opcodes or precompiles, such as stealth addresses, zkID, and confidential transactions — requires Ethereum-specific work.
https://ethresear.ch/t/post-quantum-threats-to-ethereum-privacy/24450
Current PQC migration plans assume we must verify post-quantum signatures — either on-chain (kilobytes per tx) or inside ZK circuits (millions of constraints). We present an alternative: prove authorization semantics directly in ZK, without any signature object. Result: 4,024 R1CS constraints, 128-byte proofs, 52 ms proving time. The construction is proof-system agnostic (Groth16, PLONK, STARKs all work) and deployable today as an AA validator module — no protocol changes required.
https://ethresear.ch/t/what-if-post-quantum-ethereum-doesn-t-need-signatures-at-all/24427
Speaker: xy
Lattice-based cryptography underpins major post‑quantum standards (e.g., ML‑KEM/ML‑DSA), but its strongest theoretical guarantees rely on a deep mathematical stack—geometry of numbers, linear algebra, discrete Gaussians, and Fourier analysis on lattices. This talk presents a new Lean formalization that targets this “math basement” rather than only protocol‑level game-hoppings or adversary argument: a reusable library intended to support future end‑to‑end mechanizations of worst‑case‑to‑average‑case reductions for SIS/LWE and related constructions.We mechanize core theorems and tools including Minkowski’s theorems, Poisson summation and Fourier machinery on lattices, discrete Gaussian foundations, Banaszczyk-style transference, and smoothing-parameter bounds, along with full analyses of LLL basis reduction and Babai’s nearest-plane algorithm (including non-full-rank cases). Finally, we report practical lessons from extensive LLM assistance in proof engineering: what it accelerates (library navigation and routine glue) and what still needs human design (APIs and proof architecture), with Lean’s kernel providing soundness throughout
<https://youtu.be/1O7y9t0KViA >
In this episode Nico Mohnblatt chats with Will Corcoran and Raúl Kripalani from the Ethereum Foundation. This is part 5 in the 6-part leanEthereum miniseries, shifting focus from the cryptographic primitives and LeanVM stack to the real-world integration happening through devnets, specs, and cross-team coordination.
They dive into the human coordination layer, how independent teams align on post-quantum signatures, SNARK aggregation, and protocol changes, plus the networking upgrades needed for larger payloads.
Raúl explains the shift from today's libp2p stack to a purpose-built Eth P2P next-gen version optimised for Ethereum's workloads, including better broadcast layers, erasure coding, and control planes to handle bandwidth competition between execution and consensus layers.
Speaker: Yingfei
Helger Lipmaa
Nikitas Paslis, Carla Ràfols, Alexandros Zacharakis
Dan Carmon, Lior Goldberg, Ulrich Haböck, Leonardo Lerer, Ilya Lesokhin
formalize the "flat AIR" circuit model, a modern arithmetization paradigm used by several contemporary zero-knowledge virtual machines, and we provide an in-depth security analysis of our proof of proximity for flat AIRs.
Tomas Krajci, Samuel Oleksak, Ivan Homoliak
Yunbo Yang, Yuejia Cheng, Haibo Tang, Guomin Yang, Bingsheng Zhang, Kui Ren
Pariya Akhiani, Yupeng Zhang
Kaixuan Wang, Yifan Yanggong, Chenti Baixiao, Xiaoyu Yang, Lei Wang
Anna Lysyanskaya, Eileen Nolan
Siyuan Zheng, Zhe Han
Zeyuan Yin, Leiyuan Tian, Bingsheng Zhang, Kui Ren
If you’d like to receive updates via email, subscribe to us!
ZK Circuits are a core component of integrating ZK proofs into real world applications, enabling the proving of arbitrary NP complete statements privately. A 2024 analysis revealed that approximately 96% of documented bugs in SNARK-based ZK systems were caused by under-constrained circuits, which are circuits that lack sufficient checks to prevent invalid proofs from passing verification. These vulnerabilities have enabled everything from unlimited token counterfeiting (Zcash, 2018) to $1.9 billion in forged withdrawals (zkSync Era, 2023). Thus, it is necessary to understand the security considerations when writing and designing circuits for usage in protocols and applications.
https://www.nethermind.io/blog/zk-circuit-security-a-guide-for-engineers-and-architects
This post compares the size of signatures and aggregates for transactions using Falcon signatures (as defined in the Falcon specification), under different assumptions about key recovery and aggregation.
https://ethresear.ch/t/revisiting-falcon-signature-aggregation-for-pq-mempools/24431
Industry broadly shipped PQ key exchange first (Chrome, iMessage, AWS, Cloudflare); PQ authentication is still early, especially in default public-web PKI. Ethereum inherits PQ transport encryption for some surfaces (HTTPS/JSON-RPC over TLS via Go 1.24), but application-layer privacy — cryptographic protocols built on top of the EVM rather than natively supported by opcodes or precompiles, such as stealth addresses, zkID, and confidential transactions — requires Ethereum-specific work.
https://ethresear.ch/t/post-quantum-threats-to-ethereum-privacy/24450
Current PQC migration plans assume we must verify post-quantum signatures — either on-chain (kilobytes per tx) or inside ZK circuits (millions of constraints). We present an alternative: prove authorization semantics directly in ZK, without any signature object. Result: 4,024 R1CS constraints, 128-byte proofs, 52 ms proving time. The construction is proof-system agnostic (Groth16, PLONK, STARKs all work) and deployable today as an AA validator module — no protocol changes required.
https://ethresear.ch/t/what-if-post-quantum-ethereum-doesn-t-need-signatures-at-all/24427
Speaker: xy
Lattice-based cryptography underpins major post‑quantum standards (e.g., ML‑KEM/ML‑DSA), but its strongest theoretical guarantees rely on a deep mathematical stack—geometry of numbers, linear algebra, discrete Gaussians, and Fourier analysis on lattices. This talk presents a new Lean formalization that targets this “math basement” rather than only protocol‑level game-hoppings or adversary argument: a reusable library intended to support future end‑to‑end mechanizations of worst‑case‑to‑average‑case reductions for SIS/LWE and related constructions.We mechanize core theorems and tools including Minkowski’s theorems, Poisson summation and Fourier machinery on lattices, discrete Gaussian foundations, Banaszczyk-style transference, and smoothing-parameter bounds, along with full analyses of LLL basis reduction and Babai’s nearest-plane algorithm (including non-full-rank cases). Finally, we report practical lessons from extensive LLM assistance in proof engineering: what it accelerates (library navigation and routine glue) and what still needs human design (APIs and proof architecture), with Lean’s kernel providing soundness throughout
<https://youtu.be/1O7y9t0KViA >
In this episode Nico Mohnblatt chats with Will Corcoran and Raúl Kripalani from the Ethereum Foundation. This is part 5 in the 6-part leanEthereum miniseries, shifting focus from the cryptographic primitives and LeanVM stack to the real-world integration happening through devnets, specs, and cross-team coordination.
They dive into the human coordination layer, how independent teams align on post-quantum signatures, SNARK aggregation, and protocol changes, plus the networking upgrades needed for larger payloads.
Raúl explains the shift from today's libp2p stack to a purpose-built Eth P2P next-gen version optimised for Ethereum's workloads, including better broadcast layers, erasure coding, and control planes to handle bandwidth competition between execution and consensus layers.
Speaker: Yingfei
Helger Lipmaa
Nikitas Paslis, Carla Ràfols, Alexandros Zacharakis
Dan Carmon, Lior Goldberg, Ulrich Haböck, Leonardo Lerer, Ilya Lesokhin
formalize the "flat AIR" circuit model, a modern arithmetization paradigm used by several contemporary zero-knowledge virtual machines, and we provide an in-depth security analysis of our proof of proximity for flat AIRs.
Tomas Krajci, Samuel Oleksak, Ivan Homoliak
Yunbo Yang, Yuejia Cheng, Haibo Tang, Guomin Yang, Bingsheng Zhang, Kui Ren
Pariya Akhiani, Yupeng Zhang
Kaixuan Wang, Yifan Yanggong, Chenti Baixiao, Xiaoyu Yang, Lei Wang
Anna Lysyanskaya, Eileen Nolan
Siyuan Zheng, Zhe Han
Zeyuan Yin, Leiyuan Tian, Bingsheng Zhang, Kui Ren
If you’d like to receive updates via email, subscribe to us!
Share Dialog
Share Dialog
Subscribe to ZK Insights
Subscribe to ZK Insights
<100 subscribers
<100 subscribers
No activity yet