I was always interested in formal verification but have only written toy proofs and derived programs.

It's nice to see this older discussion of the topic outside of 'AI does lean' and the assumptions that formally verification is easy or will be easy for AI and you can just switch you brain off.

Build programs that can be verified in the first place is difficult design problem that requires real thought and deep insight of the problem.