Una serie de tres partes que explica la verificación formal desde sus fundamentos, recorre el bug de solidez de Orchard de 2026 y muestra cómo Ironwood lo resolvió con una prueba matemática verificada por máquina.
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.
