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

Archetype x zkSecurity - Proof is in the Pudding: zkML

For the 11th session of Proof is in the Pudding, we teamed up with Archetype to talk about zkML. Running an LLM is already expensive. How much harder is it to prove that you ran it?

We start with what a proof of model inference actually guarantees, how inference differs from training, and the alternatives to using ZK. Then we open up a transformer and look at the computation we would have to prove.

From there, we discuss sumcheck, GKR, lookup arguments, and provers specialized for particular models. If you'd like to work through one of those building blocks yourself, our sumcheck tutorial includes code and exercises. We also covered GKR from a security angle in Session 3.

The second half looks at quantization, models designed to be easier to prove, and opportunities around KV caching. We finish with scaling, where verifiable ML might be useful, and a more speculative possibility: agents agreeing on circuits and exchanging proofs as they interact.

Jump to a topic

You can catch up on our previous session on Groth16 or browse the full series. Have a topic you'd like us to cover next? Let us know on Twitter/X!

Keep reading
Recommended

Learn Sumcheck, MLE, and HyperPlonk: An Interactive Tutorial with SageMath

A new interactive tutorial on Sumcheck, Multilinear Extensions, and HyperPlonk with complete SageMath implementations and exercises. Go beyond the theory and understand how these protocols actually work by implementing them yourself.

Marco Gaglianese · November 22, 2025

Archetype x zkSecurity - Proof is in the Pudding: Groth16

In Session 10 of "Proof is in the Pudding," we work backward from Groth16's famously compact verifier equation to explain why the protocol is shaped the way it is. We cover how R1CS constraints become polynomial identities, why pairings are needed to multiply hidden commitments, how random linear combinations and the Schwartz-Zippel lemma enforce witness consistency, and how the separating factors gamma and delta restrict which pieces of the CRS a prover can use.

ZK/SEC · July 23, 2026

Archetype x zkSecurity (Whiteboard Session) - Proof is in the Pudding: GKR and How to Prove False Statements

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!

ZK/SEC · February 25, 2025
More to explore

Kocher's Timing Attack: A Journey from Theory to Practice

Paul Kocher's 1996 timing attack showed how microsecond differences in execution time could leak private keys from RSA implementations. This tutorial recreates the attack journey from clean operation counting through noisy wall-clock measurements to sophisticated engineering solutions. Learn the variance distinguisher, explore schoolbook modular arithmetic, and discover the measurement techniques that make practical timing attacks possible despite system noise.

Martín Ochoa · September 19, 2025

Notes and Proofs for Divisor Techniques

Notes and proofs for the divisor-based ECIP protocol of Eagen, written with Diego F. Aranha and supported by MAGIC Grants. The document is self-contained: it works through the necessary algebraic geometry, the interactive proof and its soundness, the composition with a simulation-extractable NIZK, and the R1CS verifier circuit used by Parker's gadget in Monero's FCMP++.

Mathias Hall-Andersen · May 08, 2026

Comparison of formal verification frameworks for arithmetic circuits

A hands-on comparison of formal verification frameworks for arithmetic circuits, evaluating those in the ACL2 Book (r1cs, PFCS), acl2-jolt, Garden (Rocq), zk-lean, sp1-lean, and Clean. Each framework is tested on reproducibility, available examples (from basic field elements to RISC-V VM instructions), and practical verification tasks including the IsZero and weighted-sum circuits. The evaluation includes both human and Claude Code's ability to work with each framework, revealing insights about installation difficulty, proof automation capabilities, and the maturity of publicly available examples. This post maps the current landscape of formally verified ZK circuits and discusses what's coming next in this rapidly evolving field.

Yoichi Hirai · November 19, 2025