Minor nit: formal verification doesn't guarantee correctness.