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$.

In this post, we will examine one of the most interesting ways to construct zero-knowledge proofs: the MPC-in-the-Head transformation. This was first introduced in the 2007 paper Zero-knowledge from secure multiparty computation, and it is often referred to as the IKOS transformation, from the initials of the authors of the paper. The transformation allows us to construct a zero-knowledge proof system from any MPC protocol, which is treated as a black-box.

In November 2024, we discovered an inflation bug in the Aleo mainnet. We immediately reported this bug to the Aleo team. The bug was identified and then quickly fixed. Fortunately, no exploitation was detected after a thorough scan. Thanks to the Aleo team for their prompt and professional action. In this article, I will explain the context of the bug, how it could have been exploited, and how it was fixed.

In 2024, we released a paper on the security of Blockchain Rollups in collaboration with Matter Labs. The paper analyzes the security of blockchain rollups and introduces a formal model to reason about different mechanisms. You can find the paper on arxiv. In this blog post, we will discuss the security of Rollups and provide a gentle introduction to what we did in our paper. In his recent blog post, Vitalik Buterin highlighted that while Ethereum aims to be a robust, multi-purpose blockchain, there is only so much it can handle on its own.