On February 26, 2024, Renegade tasked zkSecurity with auditing parts of its circuits and smart contracts. The specific code to review was shared via GitHub as public repositories. The audit lasted 3 weeks with 2 consultants.
You can find the full report here.
We found the implementation, as well as the surrounding documentation and specifications, to be of the highest quality. The Renegade team was very responsive and helpful in answering questions and providing additional context.
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.
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.
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!
Over the past year, we've been diving into whether AI can effectively identify bugs in zero-knowledge circuits and applications, sparking questions about the future of auditing. This led us to develop SnarkSentinel, an AI-powered auditing tool. We'll share what worked, what didn’t, and how our journey with AI could impact auditing. From early challenges with Circom to innovative methods like retrieval-augmented generation and agent-led probing, we'll give you a peek into our findings, including both successes and setbacks with bug detection. Discover how AI might enhance or change the landscape of auditing and what this means for developers and security pros alike.
In June 2025, we uncovered a serious soundness issue in Solana's ZK ElGamal Proof Program that could let attackers manipulate confidential token transfers undetected. We worked with the Anza team to quickly address the flaw by pausing and disabling vulnerable components. This post dives into the root cause, which was a subtle mistake in handling prover-generated challenges within sigma OR proofs, revealing broader lessons in zero-knowledge protocol security. If you're interested in cryptographic protocol design, this could provide valuable insights.
Zero-knowledge apps are evolving, and we've been diving into their two main forms: VM instructions and arithmetic circuits. Understanding the "assembly" layer is crucial for developers, especially when optimizing and ensuring security. We’ve played around with a new toy language called **noname**, blending Golang and Rust vibes to make zkApps more understandable. With **noname**, you get detailed insights about how your code translates into gates, offering a clearer picture of the underlying "assembly" and helping pinpoint compiler bugs. If you're curious about enhancing your low-level programming skills or peeking into circuit construction, check out our experiments and see if this inspires you to create better debugging tools!
We just finished an audit of the Sui Foundation's zkLogin application and we're sharing what we found: the code is well-documented, tested, and specified. The zkLogin is set to make user authentication on the blockchain secure but simple, replacing cryptographic keys with familiar SSO methods like Google or Facebook while preserving user privacy. We also dive into the technical details behind JWT verification, non-native arithmetic for RSA, and vector programming. Plus, learn about the trusted setup process for zkLogin, ensuring maximum security through a decentralized multi-party ceremony. If you're curious about the intricate mechanics behind zkLogin, this is a must-read.
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.