Formal verification becomes one of the fundamental feature of proof system. Ziren 1.x @ProjectZKM was formally verified by Veridise, and the upcoming 2.0 is already formal verified by Lean4.
Thanks to Tachyon's @MariusMargulus, the new zk-SNARK prover in Zakura (and also in @vizorwallet) is the first Zcash prover with a machine-checked Lean proof of statistical honest-verifier zero-knowledge.
Read more:
zakura.com/engineering/ironw…
Sep 12, 2026 · 2:28 PM UTC
1
13
3,576