形式検証を基本原理から解説し、2026年のOrchard健全性バグをたどり、Ironwoodが機械検証済みの数学的証明でどう対応したかを示す全3回のシリーズ。
Research
Introduction to proving software correct instead of only testing it.
Case study of the 2026 under-constrained Orchard circuit.
How Zcash answered the Orchard bug with a machine-checked proof.