@Zcashのバグにより、Orchard支払い回路の形式的検証がIronwoodで実現されました。私はこれを愛し、支持しています。 また、@Starknetはすでに5年以上にわたり、この形式的検証を実施してきたことを強調したいと思います。 Zcashのようなプロジェクトが、今回のケースのように迅速に対応することを支援することは重要です。 同時に、Starknetのように将来に備え、先進的なプロジェクトを評価することも重要です（詳細は以下の記事をご覧ください）。 私はこれまで何度も、Starknetは他のチェーンが「まもなく実現する」と主張している機能をすでに備えているシステムだと述べてきました。これは多くの点で真実です。 私たちは、今や誰もが重要だと認識するようになった、多くの非人気な選択肢の先頭に立ってきました。たとえば、ポスト量子セキュアなZK-STARKsを最良のスケーリングおよびプライバシー解決策として採用したこと、軽量なzkVM（Cairoが最良）を採用したこと、Validiumのデータ可用性を採用したこと、そして形式的検証を採用したことです。 形式的検証とは、Leanシステムなどの自動化ツールを使用して、コードが安全であることを数学的に証明することを意味します。 コードが安全であるとは何かをすべての側面から捉えるのは非常に難しいですが、私たちのCTOである@LiorGoldberg2（Cairo zkVMおよび言語の共同開発者）の指導のもと、5年以上にわたりこの取り組みを続けてきました。 ZKに関連する主張の形式的検証に関する最初の論文（ジェレミー・アビガド教授、ヨアブ・セギナー氏ら）は、Cairo VMを定義する多項式制約の集合が正しいことを示しました。 最近のニュースをご覧になれば、AIによって発見され、現在Zcash（私が共同設立し、誇りに思い、支援している別のプロジェクト）で修正されたバグは、制約の欠落に関係していました。 このようなバグを排除するためにコードを検証するという決定は正しいステップです。CairoコアVMに対してこの種の検証を実行した結果、StarkWareチームはCairo VMに欠落した制約がないことを数学的に確信することができました。 したがって、CairoのコアVMを証明しただけでなく、コンパイラの一部であるS-two STARKシステムや、標準Cairoライブラリの多くの関数も証明しました。 仕事は完了したでしょうか？いいえ。形式的に証明可能な他の多くの要素が存在します。しかし、私たちはシステムの健全性と安全性に関わるすべてのコアプロパティを引き続き形式的に証明し続けることにコミットしています。他のプロジェクトが形式的検証を重要なツールとして受け入れているのは素晴らしいことです。StarkWareがこの分野でも先駆者であったことを誇りに思います。これが私たちにとって「将来に備えたブロックチェーン」の意味です。 さらに詳しく知りたいですか？ 以下に、過去数年間における私たちのLeanによる証明活動の詳細な記録をご覧ください。