Серія з трьох частин, що пояснює формальну верифікацію з перших принципів, розглядає помилку коректності Orchard у 2026 році та показує, як Ironwood відповів на неї машинно перевіреним математичним доказом.
Research
Introduction to proving software correct instead of only testing it.
Research
Case study of the 2026 under-constrained Orchard circuit.
Research
How Zcash answered the Orchard bug with a machine-checked proof.
