13. Executable Verification
Verify correctness by interpreting the assembly logic. Our GCD example uses the Euclidean subtraction algorithm:
#eval Nat.gcd 48 18 -- 6
#eval Nat.gcd 1071 462 -- 21
The GCD algorithm produces correct results matching Lean's built-in Nat.gcd.