형식 검증을 첫 원리부터 설명하고, 2026년 Orchard 건전성 버그를 살펴보며, Ironwood가 기계 검증된 수학적 증명으로 이에 어떻게 답했는지 보여주는 3부작 시리즈.
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.
