Proofs are often useful even if sometimes they are not "fully" trusted in some sense, and a lot of mechanisms and research in formal methods is about removing "trusted" components in viable ways. You don't even need to get especially mathematical, sometimes bog-standard engineering is enough to cover the margin of error depending on your goals... (e.g. if you have a property shown by an SMT solver to be true, you can do things like a 3-way tiebreaker and compare 3+ smt solvers for their output for a better guarantee).

The people working on formal validation tech are well aware of these limitations in the tech -- the concept of a "Trusted Basis" is a core component of the whole field, around which many techniques revolve.

Systems like seL4 use different approaches, such as "translation validation" which completely removes the need to trust a compiler toolchain, for example (because they do an automated equivalence proof between the generated assembly and a high level specification, they can just not care about the compiler). Interestingly, I know someone who worked on seL4 before its public release -- in fact at several points in the process, they got some parts of the specification wrong. You'd think this would be a death blow. But it still turned out many of these incorrect specifications weren't totally wrong, or useless at all -- in some cases they simply were not strong enough to show other desirable properties. To handwave an example: Maybe they wanted to show "No process can violate the address space of another process or halt it illegitimately" as the specification, but accidentally said "No part of the system can be put an invalid state or hung with core kernel APIs". They aren't the same thing, but it turns out, the second, 'wrong' case still eliminates a useful class of errors (while being a subset of the real specification, because to be unable to interfere with the address space of any other process or hang it somewhat implies you can't hang it, or corrupt it illegitimately, through system APIs.)

It's not (except maybe very rarely) as simple as "proof is bad" or "proof is good". There is a spectrum here along which you can assess their utility -- just like any engineering challenge.

It does take a lot of resources to do though, this is correct. The tech is improving at a pretty fast pace, and we're already getting to the point of having fully verified compilers and OSs (CompCert, seL4). It is certainly becoming more viable to do this all the time. It's still not easy, and takes a very, very different set of skills than most engineers are equipped with.

> I guess (just a guess, maybe misinformed) that proper testing and fuzz testing of code is considerably more beneficial than finding bugs by trying to prove it.

For average software, this is true, but it's mostly a cost question. Frankly you don't need mathematics to make shit, insecure software less insecure, you can absolutely improve them without that.

But they don't really do the same thing anyway; proofs show a mathematical absence (or prove a mathematical fact) of certain classes of errors. Fuzzers can only show the existence of certain errors -- they cannot definitively prove anything other than "Some bugs exist".

There was a paper recently (I can't find it) that explored this idea; essentially the authors injected obvious, "should-be detectable" bugs into many pieces of software, then ran fuzzers over the software to see how many of the injected bugs could be found. The takeaway was, IIRC: fuzzers didn't find anything close to the real number of injected bugs, not even considering bugs that weren't found and were not injected by the authors. Which means that despite their automation triumphs, we could very easily be missing real, catastrophic errors, at a very high rate.

Fuzzers haven't definitively proven that there isn't another Heartbleed out there, somewhere.