THREE WAYS FORMALLY VERIFIED CODE CAN GO WRONG IN PRACTICE

Summary from the TLDR Dev newsletter

Formally verified code, despite being "correct" according to specifications, can still contain bugs in practice. These bugs arise from three main issues: invalid proofs, incorrect properties being verified, and wrong assumptions made during the verification process. "Correctness" in formal methods refers to conformity with a specification, which may not always align with real-world expectations or cover all potential issues.