- Formally verified code can still have bugs if the proof itself is invalid, such as due to a bug in the theorem prover or using unproven assumptions (shortcuts).
- Bugs arise when the properties (specifications) being proven are wrong or weaker than needed, like the leftpad example proving string length instead of visual alignment for Unicode.
- Assumptions, such as environmental conditions or unverified dependencies, can break correctness even if the proof is valid, as seen in binary search overflow issues or reliance on external services.