>I find it much easier to formally verify things correct than to test that they're correct.

This rise in me the famous joke by Knuth: Beware of bugs in the above code; I have only proved it correct, not tried it.

I wonder which tools he uses to prove correctness, and on which language. I know about Frama-C, Coq, and things like that. But I never had the opportunity to use them out of university. On the same topic, in a recent ACM publication, Ian Joyner compare Frama-C with a lipstick on a Pig.

https://cacm.acm.org/magazines/2021/12/256941-common-ails/fu...