Barrett reduction is a widely used algorithm for reducing a value modulo $m$. Our analysis, conducted during the Rust p256 crate audit, shows that the error bound for Barrett reduction can be tighter than traditionally assumed. For most moduli used in cryptography (e.g., NIST curves), the quotient approximation error is at most 1 (not 2). This improvement eliminates the need for a second subtraction in practice. By adopting this optimization, RustCrypto p256 achieves a 14% performance improvement in scalar multiplication.
A polynomial commitment scheme (PCS) allows a prover to commit to a polynomial and later prove its evaluations at points chosen by the verifier. The verifier can then check that the evaluations are consistent with the committed polynomial. Most practical SNARKs (Succinct Non-interactive Arguments of Knowledge) are constructed using a PCS. It consists of the following three algorithms: $setup(d) \rightarrow pp$: Given an upper bound $d$ on the degree, it outputs public parameters $pp$ used to commit to polynomials of degree less than $d$.
Client-side proving is crucial for enabling privacy-preserving ZK applications, yet there are still two main bottlenecks: time and space (memory constraints). There are many technical breakthroughs that address these constraints such as: Incrementally verifiable computation (IVC) techniques Accumulation (Halo2) Folding (Nova, Hypernova, Protostar) Recursion (Plonky3, Starknet, RiscZero) Degelating proof generation Full proof delegation to trusted execution environments (TEEs) Full proof delegation via coSNARKs (e.g. zkSaaS) Partial proof delegation by separating a circuit into private and public computations (Aztec’s zk-rollup) Streaming the witness (Gemini, Ligetron) Yet another approach is leveraging GPUs, which significantly boost performance for parallelizable tasks.
We are really excited to share our initial steps towards building clean, an embedded DSL and formal verification framework for ZK circuits in Lean4. As we recently shared, Zero Knowledge circuits are full of bugs, but fortunately, techniques like formal verification can provide a huge confidence boost in the correctness of ZK circuits. Clean enables us to define circuits in Lean4, specify their desired properties, and – most importantly – formally prove them!
Earlier this year, we had the chance to work with Celo on a security audit of the Self project—a new approach to on-chain identity built around biometric passports and zero-knowledge proofs. Over the course of three weeks, we reviewed core components of the protocol: cryptographic primitives (including ECDSA and RSA implementations in Circom), key circuits and smart contracts, and a TEE-based proof delegation system built on AWS Nitro Enclaves.
Bitcoin has long been considered limited in its ability to verify arbitrary computations (including verifying zero-knowledge proofs!). However, recent developments of BitVM variants have shown the potential to verify arbitrary computations on Bitcoin without modifying its core protocol. The BitVM1, which is formalized in an eprint paper, introduced the circuitry idea to enable arbitrary computation on Bitcoin. It employs an optimistic protocol where computations can be done off-chain, and resolved on-chain among the roles of proposer and challenger when there is a dispute over the computations.
Zero-knowledge Virtual Machines (zkVMs) leverage zero-knowledge proofs (ZKPs) to verify the correctness of computations executed on a specific instruction set architecture. In practical terms, zkVMs allow you to write programs in familiar high-level languages — such as Rust or C — without having to deal with the details of ZKPs. By abstracting these complexities, a secure zkVM can generate and verify proofs for any application. In this post, we give a brief refresher on zkVMs and discuss several projects that have significantly influenced their design and evolution.
In this third whiteboard session in partnership with Archetype, we explain how a recent paper on Fiat-Shamir security and the GKR protocol works.
Looking for an internship in ZK, MPC, FHE, and post-quantum cryptography? Interested in working with AI, formal verification, and TEEs? We are always looking for talented peeps to join our team and do interesting research! Here are some of the projects our previous interns have worked on: Reproducing and Exploiting ZK Circuit Vulnerabilities A Technical Dive into Jolt: The RISC-V zkVM An Introduction to Interactive Theorem Provers Circle STARKs: Part II, Circles The fast track to get an interview is to solve our zkBank challenge, but feel free to apply directly by submitting your resume to internships2025@zksecurity.
In this post we start our journey into the algebra of Circle STARKs. It’s pretty easy actually. The Complex Numbers You remember the complex numbers $\mathbb{C}$ from high-school maths, right? Some high-school teachers are better at conveying this than others, but the way to “construct” the complex numbers is as a quotient of the polynomial ring $\mathbb{R}[X]$ by the ideal generated by the irreducible polynomial $X^2 + 1 \in \mathbb{R}[X]$: $$ \mathbb{C} = \mathbb{R}[X] / (X^2 + 1) $$ In other words, polynomials plus/minus multiples of $X^2 + 1$.