IMO formal software verification is still waaay too difficult to be worth it in all but the most extreme cases. That's really different to formal hardware verification where it is a no-brainer.

I keep trying to learn it, but you need to be a real expert. Like "I wrote the compiler" level expert for most systems.

For example I tried to prove a varint encoder/decoder. It worked for one or two bytes, but not more. Asking for help the reason was that the compiler internally only unrolls loops 5 times, or some random internal detail like that that you could never really hope to know.

I've been learning Lean recently, and ... I mean I like it, but if you learn it you're going to encounter documentation like this:

> Definitional equality includes η-equivalence of functions and single-constructor inductive types. That is, fun x => f x is definitionally equal to f, and S.mk x.f1 x.f2 is definitionally equal to x, if S is a structure with fields f1 and f2. It also features proof irrelevance, so any two proofs of the same proposition are definitionally equal. It is reflexive, symmetric, and a congruence.

And that's not really a knock on Lean - it seems to have some of the better documentation out of the alternatives.