币圈界报道，6月5日ZEC受Orchard池无限伪造漏洞影响大跌30%，ZODL创始人Josh Swihart发文表示，Orchard漏洞存在于其中一条规则中，该规则编写得过于宽松，允许接受虚假信息并仍然通过验证。因此，引擎可能会误认为虚假交易有效。实际上，有人可能在Orchard交易池中伪造了ZEC。这是手写规则中的缺陷，而不是底层密码学或生成证明的引擎中的缺陷。问题是如何确保漏洞不再发生，最好的答案是形式化验证。Tachyon 目前正采用形式化验证进行构建，使用更简洁、更统一的规则手册。与 Orchard 相比，特殊情况和复杂细节更少，这意味着整个规则手册都可以通过数学证明进行完美验证。多个团队已经在着手正式验证Orchard现有的电路。如果验证成功，那么在Tachyon之前，近期推出第二个Orchard池或许是最佳方案。Tachyon更加简洁，但经过正式验证的Orchard池可以作为有效的过渡措施。