Proof is in the Pudding · Part 4 of 11

Archetype x zkSecurity - Proof is in the Pudding: TEEs with Intel TDX

ZK/SEC June 28, 2025 1 min educative · TEE · security

For the 5th session of Proof is in the Pudding, we teamed up with Archetype to whiteboard an introduction to Trusted Execution Environments (TEEs).

In this session, we unpacked the fundamentals of TEEs and their role in confidential computing, focusing on how they protect data while it’s being used, not just at rest or in transit. We explored current technologies like Intel TDX, AMD SEV-SNP, ARM CCA, AWS Nitro Enclaves, and even Nvidia’s approach to secure GPU computing. (BTW check out our audit of Self on their use of Nitro enclaves!)

We also traced the evolution of TEEs: from early enclave models like Intel SGX to today’s Confidential VMs and Confidential Containers. Along the way, we broke down core TEE properties like integrity (ensured through remote attestation) and confidentiality (secure computation on encrypted data). The session didn’t shy away from real-world challenges either, covering attack surfaces, the Trusted Computing Base (TCB), and the complexities of secure system design.

The deep dive concluded with a technical look at Intel TDX, illustrating how it extends existing virtualization layers to enforce strong isolation using memory encryption and cryptographic measurements.

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

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 (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

AI meets Cryptography 3: What AI Found in Bron Labs's bron-crypto

We pointed our AI audit pipeline at bron-crypto, Bron Labs's Go library for MPC and threshold signatures, and confirmed four bugs. All of them are now fixed upstream. This is the third post in our series on bugs our agents found across open source cryptography.

Stefanos Chaliasos, Hao Pham · July 22, 2026

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 and Fixing an Inflation Bug in 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.

Suneal Gong · February 19, 2025