तीन भागों की एक श्रृंखला जो मूल सिद्धांतों से औपचारिक सत्यापन को समझाती है, 2026 के Orchard साउंडनेस बग पर चर्चा करती है, और दिखाती है कि 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.
