Whenever you look closely at what these proof nerds have actually built you typically find… nothing. No offense to them, it’s simply reality.
I might also point out FM had a nice history of value-add in HW. And we know HW is higher quality than software.
Formal methods are the hardest thing in programming, second only to naming things and off by one errors.