Project Tachyonによると、火曜日にZcashの研究者がIronwoodの形式的検証を完了し、ネットワークの新しいシールドプールが、定められた暗号学的前提のもとでは検出不能な偽造（カウンターフィット）バグを含まないことを示す、機械チェック済みの証明を公開しました。
この証明はLeanというプログラミング言語で書かれており、2,700件超の定理で構成され、1か月以上にわたって3つの研究・暗号チームが完成させました。この作業によりバランスの完全性が確立され、シールドプールが公開されている入力額を超えて価値を支払えないことが保証されます。この証明はIronwoodのゼロ知識証明システム、回路ルール、台帳レベルでの会計を対象にしていますが、プライバシー保証については扱っていません。
