سلسلة من ثلاثة أجزاء تشرح التحقق الرسمي من المبادئ الأولى، وتستعرض خلل سلامة 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.
