
In this third whiteboard session in partnership with Archetype, we explain how a recent paper on Fiat-Shamir security and the GKR protocol works.

In this third whiteboard session in partnership with Archetype, we explain how a recent paper on Fiat-Shamir security and the GKR protocol works.
Mathias and Giorgio join Anna Rose and fellow zkSecurity teammates Nico and Kobi on the Zero Knowledge podcast to talk about Clean, zkGolf, and what happens when AI agents compete to build better circuits with proofs of correctness.
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.
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.
Join us for a deep dive into the fascinating world of arithmetization as David from our team breaks down the process of converting logical statements into algebraic forms to create arithmetic circuits, essential for constructing ZK proofs. This unedited recording from our "Proof is in the Pudding" series offers a unique opportunity to grasp these foundational concepts, perfect for anyone keen on unlocking the mechanics behind zero-knowledge proofs. Curious? Check out the session on Archetype's channel!
In our "Proof is in the Pudding" series, hosted with Archetype, we dive into the world of zkTLS, also known as zkOracles, HTTPz, or MPC-TLS. You'll get the inside scoop on various approaches like public oracles, TEE methods such as TownCrier, and hybrid models using MPC protocols. It's a perfect chance to explore cutting-edge TLS technologies and see how they shape secure communication. Check out the recorded session on Archetype's channel!
In the latest session of "Proof is in the Pudding," we teamed up with Archetype to explore the basics of Trusted Execution Environments. Through a collaborative whiteboarding session, we break down key concepts and practical applications, making this tech topic accessible and engaging. Dive in to discover how these environments can enhance digital security in a straightforward way.
In this final part of our series on Circle STARKs, we tie together concepts from Mersenne prime fields, circle curves and bivariate polynomials to showcase a comprehensive Circle STARK protocol. We detail the process of arithmetization over the circle curve, introducing Circle FRI as a low-degree test and walk through the complete Circle STARK construction. Readers will explore how trace commitments, constraint batching and low-degree proofs combine for efficient verifiable computation, delving into the nuances of proof validity and security analysis.
We’ve teamed up with Matter Labs and Sigma Zero to dive deep into the security of Byzantine Fault Tolerant (BFT) consensus protocols. In our new paper, we explore real-world vulnerabilities found in BFT systems, including popular algorithms like BA*, HotStuff, and Paxos. You'll discover insights into subtle bugs, cryptographic issues, and the challenges of translating theoretical models into secure, working code. Whether you’re designing or implementing these protocols, our findings offer valuable lessons and strategies for creating more secure and reliable distributed systems. Check it out, it’s a must-read for anyone working with BFT!
Curious about diving into zero-knowledge (ZK) application development? Our blog post is here to guide you through the common security pitfalls and mindset shifts essential for tackling ZK programming. We reflect on our journey from the early days of Mina Protocol to the dynamic space today, filled with tools like SnarkyJS and newer approaches to split the prover and verifier roles effectively. Discover the errors to avoid, like under-constraining data and letting divisors slip through unchecked, and learn how a solid review and audit process can save your ZK applications from disastrous security issues. Dive in to get the insights you need to navigate the ZK landscape confidently!