Eine dreiteilige Reihe, die formale Verifikation von Grund auf erklärt, den Orchard-Soundness-Bug von 2026 erläutert und zeigt, wie Ironwood ihn mit einem maschinell geprüften mathematischen Beweis beantwortete.
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.
