@argumentxyz team open-sourced Ix, a zero-knowledge proof-carrying code platform, which can compile Lean 4 programs into zk-SNARKs, implement program execution and type checking verification, significantly reducing the running cost of verification. @argumentxyz 团队开源了Ix平台,该平台能够将Lean 4程序编译成zk-SNARKs,实现程序的执行和类型检查验证,显著降低验证的运行成本。 @argumentxyz チームがオープンソース化した Ix は、Lean 4 プログラムを zk-SNARK にコンパイルし、プログラム実行と型チェック検証を実行できるゼロ知識証明付きコードプラットフォームであり、検証の実行コストを大幅に削減します。
@0xPolygon and @IrreducibleHW team open-sourced PetraVM, a general-purpose virtual machine based on the Binius proof system, supporting recursive proof verification and high-performance computation, through WebAssembly compilation and a custom high-level language PetraML. @0xPolygon 和 @IrreducibleHW 团队开源了PetraVM,一个基于Binius证明系统的通用虚拟机,支持递归证明验证和高效计算,通过WebAssembly编译和自定义高级语言PetraML实现高性能可验证计算。 @0xPolygon と @IrreducibleHW チームは、Binius 証明システムに基づいた汎用仮想マシンである PetraVM をオープンソース化しました。これは、WebAssembly コンパイルとカスタムの高級言語 PetraML を介して、再帰的証明検証と高性能計算をサポートします。