The @Zcash bug leads to Ironwood, formal verification of the Orchard payment circuit. I love and support it. I also want to stress that @Starknet has been doing that -- formal verification -- for over 5 years. It's important to support great projects like Zcash for reacting quickly, as in this case. It’s also important to recognize projects that are future-proof and ahead of the curve, like Starknet. (Details in the article below) I’ve said often that Starknet is that system which already has the stuff other chains claim they soon will. It's been true for many things. We've been at the vanguard of many unpopular choices that now everyone recognizes are important, including post-quantum secure ZK-STARKs as the best scaling and privacy solution, lean zkVMs (Cairo is best), Validium data availability, and formal verification. Formal verification means that you use automated tools like the Lean system to mathematically prove that your code is safe. It's very hard to capture each and every aspect of what it means for code to be safe, but led by our CTO @LiorGoldberg2 (co-creator of Cairo zkVM and language), we've been at it for more than 5 years. The very first paper on formal verification of claims related to ZK (Professor Jeremy Avigad, Yoav Seginer, and others) showed that the set of polynomial constraints defining the Cairo VM is correct. If you've been following the news lately, the bug that was recently discovered by AI and now fixed for Zcash (another project I co-founded, and which I'm very proud of and support) had to do with a missing constraint. The decision to verify their code to rule out other such bugs is the right step. Running this kind of verification for the Cairo core VM provided us, the StarkWare team, with mathematical certainty that there is no missing constraint in our Cairo VM. So, in addition to proving the core VM of Cairo, we have also proved the S-two STARK system, part of the compiler, and many of the functions in the standard Cairo library. Is the job done? No. There are a lot of other things that can be proven formally . But we are committed to continuing to formally prove all the core properties that have to do with the soundness and safety of our systems. It's great to see other projects embracing formal verification as an important tool. I'm proud that StarkWare led the path in this aspect too. That’s what Future Proof blockchain means to us. Want to learn more? Here's a detailed account of our Lean proving efforts over the past few years