Featured
Giorgio Dell'Immagine
March 27, 2025
11 min read
announcement
tools
zk
formal-verification
We're diving into our new project called **clean**, aimed at creating an embedded DSL and formal verification framework for Zero Knowledge (ZK) circuits using Lean4. Imagine being able to not only define ZK circuits but also formally prove their correctness—sounds like a game-changer, right? We'll walk you through our process of building a robust library of reusable, verified circuit gadgets, focusing on the importance of soundness and completeness. Plus, you'll get a peek at some cool examples like 8-bit addition and how we're tackling ZKVM design with techniques borrowed from Fibonacci sequences. It's exciting stuff, and if you're curious about how we're paving the way for bug-free ZK circuits, this is a read you won't want to miss!
Read →
ZK/SEC
March 24, 2025
1 min read
educative
security
zk
audit
identity
We recently teamed up with Celo for an in-depth security audit of the Self project, exploring its innovative approach to on-chain identity using biometric passports and zero-knowledge proofs. During our three-week dive, we examined everything from cryptographic primitives to smart contract architecture and a unique proof delegation system using AWS Nitro Enclaves. The Celo team impressed us with their commitment and responsiveness, and we collaborated on refining the system with strategic improvements. Curious about the nitty-gritty details and our insights? Check out the full report!
Read →
Katat Choi
March 03, 2025
17 min read
educative
zk
bitcoin
We're diving into the world of Bitcoin's UTXO model and how recent advancements like BitVM can overcome its limitations, allowing for more complex computations without changing Bitcoin's core. This blog post explores cutting-edge techniques like covenants, statefulness, and circuit models, showing how they enable intricate logic on Bitcoin. We'll break down how these innovations make trustless cross-chain transactions possible, and highlight the potential of optimistic protocols to optimize the on-chain footprint. If you're curious about the future of Bitcoin's capabilities, this is the deep dive you need!
Read →
Marco Besier, David Wong
February 26, 2025
12 min read
educative
zk
zkvm
Curious about how zero-knowledge virtual machines (zkVMs) make computing more secure without the hassle? We delve into the fascinating world of zkVMs, where you can program in high-level languages like Rust or C and let cryptography handle the complexity. We'll explore the evolution of these innovative systems through projects like Cairo and RISC Zero, while touching on the unique benefits and technical insights each brings. Plus, learn about groundbreaking techniques for optimizing zkVMs with projects like Jolt, and discover a range of other influential zkVM initiatives. Get ready for an enlightening journey into secure computation!
Read →
ZK/SEC
February 25, 2025
1 min read
announcement
Thinking about diving into the world of cryptography and cutting-edge tech? We're on the lookout for bright minds to join us for internships in areas like ZK, MPC, and post-quantum cryptography. Our past interns have tackled exciting projects like exploring ZK circuit vulnerabilities and delving into RISC-V zkVMs. If you want a fast track to an interview, try out the zkBank challenge, or simply send us your resume. Come join us and see where the journey takes you!
Read →
ZK/SEC
February 25, 2025
1 min read
educative
security
zk
gkr
In our third whiteboard session with Archetype, we dive into the fascinating world of cryptographic protocols by breaking down the intricacies of the Fiat-Shamir security model and the GKR protocol. Whether you're a cryptography enthusiast or just curious about how these complex mechanisms enhance security, this is a chance to explore the theories with us in a friendly and digestible way. Don't miss the opportunity to expand your understanding of this cutting-edge topic!
Read →
Varun Thakore, Mathias Hall-Andersen
February 21, 2025
16 min read
educative
zk
fri
In this blog post, we dive into the fascinating world of Circle STARKs, exploring the algebra of complex numbers and how they can be extended to any field. We revisit the concept of the unit circle and its unique group structure, which allows for cool operations like squaring and doubling angles. You'll discover how these ideas apply to finite fields, creating intriguing structures like the twin-coset and standard position coset. The post leads us to understand vanishing polynomials, crucial in STARKs, and sets the stage for exploring the circle FFT in upcoming discussions. Perfect for anyone curious about cutting-edge cryptographic techniques!
Read →
Giorgio Dell'Immagine
February 20, 2025
13 min read
educative
zk
MPC
In this blog post, we dive into the fascinating world of zero-knowledge proofs using the MPC-in-the-Head transformation—a clever method that constructs proof systems from any secure multiparty computation protocol. Originally proposed in 2007, this transformation uses a creative approach involving "imaginary parties" to prove knowledge without revealing it. We explain how this technique can be applied to develop post-quantum signature schemes, providing insights into its practical implications and efficiency. By exploring these concepts, readers will uncover a unique intersection of cryptography and computer science.
Read →
Suneal Gong
February 19, 2025
13 min read
security
zk
audit
aleo
In November 2024, we found a significant inflation bug in the Aleo mainnet that could have allowed token minting without proper checks. We immediately informed the Aleo team, who swiftly addressed the issue with no detected exploitation. This post dives into the inner workings of Aleo and explains how transitions and records operate, providing insight into how the vulnerability was discovered and resolved. It's an intriguing look at blockchain security, zero-knowledge proofs, and the importance of thorough type checks to ensure robust protocol integrity.
Read →
Stefanos Chaliasos
February 18, 2025
6 min read
educative
security
zk
formal-verification
In our latest blog post, we dig into the fascinating world of blockchain rollups, focusing on their security and how they help Ethereum scale while maintaining its core values of decentralization. We'll break down the concepts of Optimistic and ZK-Rollups, discuss the importance of projects like L2BEAT in assessing rollup maturity, and introduce our formal model for ensuring rollup security. If you're curious about how forced transactions, safe blacklisting, and upgradeability are shaping the future of Ethereum, this is a read you won't want to miss.
Read →
Stefanos Chaliasos
February 17, 2025
3 min read
announcement
security
tools
zk
We're thrilled to introduce our new site, [bugs.zksecurity.xyz](https://bugs.zksecurity.xyz/), a hub for exploring past vulnerabilities in ZK circuits. Dive into our growing catalog of documented bugs and learn how we've reproduced some with comprehensive scripts. Discover evaluations of prominent security tools like Circomspect and Picus, and see where they shine or stumble. We're calling on the community to join us in expanding this invaluable resource—whether by adding bugs, reproducing them, or improving our platform. Let's collaborate to elevate ZK security together!
Read →
Marco Besier
February 04, 2025
5 min read
educative
tools
formal-verification
Kevin Buzzard, a mathematician with a cautious view on human-checked proofs, found solace in interactive theorem provers, which verify mathematical proofs much like type-checking in programming. We explore how these tools, which are gaining traction in fields like applied cryptography, ensure rigorous and reliable proofs. With Lean as our focus, you'll discover how to dive into this fascinating world, see a proof in action, and learn how this technology is revolutionizing areas like zero-knowledge virtual machines. Curious about building rock-solid, machine-verified proofs? Check out our beginner-friendly guide!
Read →