We're always on the lookout for passionate people to join us to work on the most exciting projects in the ZK space. If you love finding bugs and are interested in ZK, you might want to take our new challenge: zkBank.
This challenge is for everyone, and you'll have to learn a bit of everything to solve it. If you think you have what it takes, then give it a go: https://github.com/zksecurity/zkBank/tree/main
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.
Think you have what it takes to join zkSecurity? We're raising the bar with a second challenge! Now candidates must complete both zkBank and our new Curve Machine challenge to prove their skills across the full spectrum of ZK security. Are you ready to take on both challenges?
We're thrilled to introduce our new site, [bugs.zksecurity.xyz](https://bugs.zksecurity.xyz/), a hub for exploring past vulnerabilities in ZK circuits. Dive into our growing catalog of documented bugs and learn how we've reproduced some with comprehensive scripts. Discover evaluations of prominent security tools like Circomspect and Picus, and see where they shine or stumble. We're calling on the community to join us in expanding this invaluable resource, whether by adding bugs, reproducing them, or improving our platform. Let's collaborate to elevate ZK security together!
Check out our latest blog post where we dive into the world of Zero-Knowledge Proof (ZKP) vulnerabilities, sharing our insights from replicating known ZK circuit weaknesses. We’ve launched a GitHub repo with detailed scripts to help you understand, reproduce, and learn from these vulnerabilities. Discover how this hands-on approach aids in grasping attack vectors, testing fixes, and enriching educational resources. Whether you're a researcher or a developer, this post is packed with info to enhance your knowledge and skills in ZKP security. Plus, find out how you can contribute to expanding this invaluable resource!
An intuition-first walkthrough of why 33% BFT needs two voting rounds, how 20% designs get true one-round finality, and how an optimistic fast path can bridge the gap.
Kevin Buzzard, a mathematician with a cautious view on human-checked proofs, found solace in interactive theorem provers, which verify mathematical proofs much like type-checking in programming. We explore how these tools, which are gaining traction in fields like applied cryptography, ensure rigorous and reliable proofs. With Lean as our focus, you'll discover how to dive into this fascinating world, see a proof in action, and learn how this technology is revolutionizing areas like zero-knowledge virtual machines. Curious about building rock-solid, machine-verified proofs? Check out our beginner-friendly guide!
A month after launching mpcsec.org, we added a searchable tracker of real-world MPC bugs, expanded the pitfall taxonomy, published contribution templates and refreshed the site UI.