ZK/SEC Research notes from zkSecurity
All posts
Proof is in the Pudding · Part 9 of 11

Archetype x zkSecurity - Proof is in the Pudding: ZK on Bitcoin

ZK/SEC April 02, 2026 2 min educative · zk · bitcoin

For the 9th session of Proof is in the Pudding, we teamed up with Archetype to explore ZK on Bitcoin.

Bitcoin's UTXO model and limited scripting language create unique challenges for verifying zero-knowledge proofs. In this session, we walk through the fundamental constraints of Bitcoin Script and then explore the creative approaches that have been developed to bring ZK verification to Bitcoin, from multi-party computation techniques to BitVM's optimistic verification paradigm.

We covered:

  • UTXO Model vs Account Model: The fundamental differences between Bitcoin's transaction model and Ethereum's account-based approach, and why this matters for ZK
  • Bitcoin Script Limitations: Why Bitcoin's intentionally constrained scripting language makes direct ZK proof verification so challenging
  • Verifying ZK proofs in Bitcoin Script: The core problem and early approaches to on-chain ZK verification
  • ZK Bitcoin (MPC Approach): Using multi-party computation to enable ZK proof verification without native script support
  • BitVM: Optimistic Verification: How BitVM brings expressive computation to Bitcoin through an optimistic execution model with fraud proofs
  • Timelocks and Forcing Progress: Using Bitcoin's timelock mechanisms to ensure protocol liveness
  • Statelessness Problem: Why Bitcoin's stateless design creates challenges for multi-step protocols
  • Lamport Signatures for State: How Lamport signatures can simulate state across Bitcoin transactions
  • Taproot: How Bitcoin's Taproot upgrade enables more complex scripting while preserving privacy
  • Simulated Covenants: Techniques for achieving covenant-like behavior on Bitcoin without native covenant support
  • BitVM Fraud Proof: The mechanics of how BitVM's fraud proof system works in practice
  • BitVM 3, Hashlocks, and Garbled Circuits: The next evolution of BitVM using garbled circuits and hashlock-based verification
  • Cut-and-Choose Security: The cryptographic technique that underpins the security of garbled circuit protocols
  • Witness Encryption (BABE): How witness encryption opens up new possibilities for Bitcoin programmability

If you enjoy this video, check out our previous episodes:

Have a topic you'd like us to cover in a future session? Let us know on Twitter/X!

Keep reading
Latest

Checking the Checkers and Auditing the Ironwood FV

Cryptographic software is error-prone and failures are catastrophic, therefore formal verification is a powerful and increasingly practical tool for greatly improving the assurances of our cryptographic software. But who verifies the formal verification? Formal verification itself is software too, what is proved, under which assumptions and its relation to the real-world implementation lie beyond the scope of the machine-checked proof. In this post, we want to give some insights into our three-week audit of the Ironwood formalization and some of the common pitfalls that formal verification more broadly can encounter.

Mathias Hall-Andersen · October 05, 2026

Archetype x zkSecurity - Proof is in the Pudding: zkML

In Session 11 of "Proof is in the Pudding," we look at what it takes to prove model inference. We cover transformer computation, sumcheck, GKR, lookup arguments, quantization, and KV caching, then discuss scaling and possible uses for verifiable ML.

ZK/SEC · September 30, 2026

Intro to Clean for Devs.

We think that Clean is the future of circuit development, so we created a programmer-first introduction to show circuit developers who have never used formal verification how they can build circuits faster, safer and better.

Mathias Hall-Andersen · September 29, 2026
Recommended

Archetype x zkSecurity - Proof is in the Pudding: Privacy in Payment Networks

In Session 08 of "Proof is in the Pudding," we explore how different networks have approached privacy over the years. From E-Cash and Monero to MobileCoin and Zether, we break down blind signatures, Pedersen commitments, stealth addresses, ring signatures, and more. This session provides a comprehensive tour of the techniques used to break linkability, hide addresses, and obscure transaction data in the name of privacy and safety.

ZK/SEC · January 16, 2026

Archetype x zkSecurity - Proof is in the Pudding: The Other Dark Forest (Offchain Public Keys)

In Session 07 of "Proof is in the Pudding," we explore the other dark forest, the realm of offchain public keys. We dive into zkLogin, ZK Email, and ZKPassport, examining how these protocols handle authentication and privacy. We also discuss the issue of unlinkability in privacy protocols and why replacing traditional signature verifications with zero-knowledge proofs could unlock more interesting and powerful ZK products.

ZK/SEC · October 21, 2025

Archetype x zkSecurity - Proof in the Pudding: Introduction to Data Availability (Sampling)

In the latest "Proof is in the Pudding" session, we team up with Archetype to break down the essentials of Data Availability Sampling. We dive into how rollups and Ethereum's DA system work, explore the role of DA chains, and touch on the basics of verifiable sharding. This introduction is perfect for anyone curious about the foundations of data availability sampling and how these concepts are playing out in the blockchain world.

ZK/SEC · October 02, 2025
More to explore

Why does FRI work?

This blog post explains the security intuition behind the FRI protocol, which proves that a function is close to a valid Reed-Solomon codeword. It introduces the "prover message graph," a layered structure that visualizes how correct and incorrect folds affect verification. We conclude that if too many folds are inconsistent, the verifier will likely reject, but if most are correct, the initial function must be close to a proper codeword.

Nicolas Mohnblatt · October 30, 2025

Uncovering the Query Collision Bug in Halo2: How a Single Extra Query Breaks Soundness

We recently discovered a subtle but important soundness issue in Halo2, which we’ve named the query collision bug. It affects certain edge-case circuits and was present in widely used versions, including the main Zcash implementation and PSE’s fork. We disclosed the issue to the relevant teams, including Zcash, PSE, and Axiom, all of whom have since patched it. While no known production circuits were affected, the bug reveals a surprising vulnerability in the proving system that deserves attention.

Suneal Gong · July 09, 2025

ZPrize Came To An End! Who And How Did They Win $500,000?

In an exciting collaboration with ZPrize, we embarked on a journey to discover the fastest proofs for ECDSA signatures, ultimately crowning two standout approaches as winners. The blog post delves into the innovative solutions that captured the $500,000 prize by pushing the boundaries of zero-knowledge proofs. The story offers a fascinating glimpse into how these cutting-edge techniques might pave the way for privacy-focused applications. Curious to know which teams came out on top and how they did it? Dive in to explore the thrilling results and what's next in the ZK space!

ZK/SEC · May 06, 2024