Three ways formally verified code can go wrong in practice
buttondown.com
"Correct" doesn't mean "correct" when correctly using "correct"