Una serie in tre parti che spiega la verifica formale dai primi principi, analizza il bug di solidità di Orchard del 2026 e mostra come Ironwood vi ha risposto con una prova matematica verificata da una macchina.
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.
