Testing cannot be used to prove that a flaw doesn't exist, only that it does.
FWIW, I wrote a similar blog post about a different encryption bug that really seemed like it should have been found by fuzzing, and had 100% coverage.
https://googleprojectzero.blogspot.com/2021/12/this-shouldnt...
Not that I disagree with you, just a practical example.
It would be interesting to find a way to create excursions into these various parameter spaces but some of them are baked into the infrastructure in such a way that it makes it difficult.
This is not universally true, formal methods can take you a long way, depending on the problem domain.
And sometimes you can test for every possible input. This usually isn't feasible, but it's nice when it is.
As you say, though, exhaustive testing is sometimes possible.
The whole program? Yes.
For testing individual components, there's no need to assume. The answer is very likely either clearly yes (the input is a handful of booleans) or clearly no (the input is several integers or even unbounded) and for those cases where it's not immediately clear (one i16? Three u8s?) it's probably still not hard to think through for your particular case in your particular context.
[1] https://randomascii.wordpress.com/2014/01/27/theres-only-fou...
Whether 4B is doable depends on how much work you're doing for each of those states, but yes, "4B" alone certainly doesn't rule it out. There's also a question of whether it goes with your most frequently run tests or is something that's only run occasionally.
> However a lot of algorithms can have more than 32 bits of states and so quickly get beyond what is doable.
I'm pretty confident we're all in agreement there.
The work done by a a theorem prover and a fuzzer isn't all that different (and sufficiently advanced fuzzers use SMT solvers etc.)
Also, how is even "smart fuzzing" similar to theorem provers in any way? Fuzzers still think in terms of runs, but a theorem considers all cases. The best fuzzer wouldn't be able to tell if a sort algorithm works for all inputs, presuming the input size is unbounded. Actually, my understanding is that a fuzzer wouldn't be able to prove if identity function works for all kinds of objects it may be given.
The famous Donald Knuth has also stated "Beware of bugs in the above code; I have only proved it correct, not tried it.", which again hints that there are limits to proved programs.
I'll admit that I don't know much about them, what I know meringues me - but I can't figure out how to use them in the real world. However I know enough to know that they are not perfect.
TLA+ is very useful, but it's not going to prove out your software itself, that will require testing or other methods, it will help prove out your specification. I've used it to good effect both for designing distributed and concurrent systems and for identifying issues in existing systems (without an existing formal spec, by creating it and then playing with the invariants and other aspects of the TLA+ spec). SPARK/Ada, I mentioned in my other comment, will detect many problems, and help you prove the absence of many others. But it's also not suitable (yet) for all projects, or more than a subset of a project, since it has specific limitations on what it can prove and is only compatible with a subset of Ada (this is being expanded each year). The subset of Ada it does apply to is actually quite significant and useful, but you have to be capable of understanding that it is limited and then apply it within that limited scope.
This is true for every other formal method approach I've seen. Pay attention, read, ask questions, and don't judge them all by one paper you half remember from 42 years ago.
But the trick is to remember making the specification model the real world at sufficient detail: not too detailed to make the specification unwieldy, not too relaxed to skip real real-world issues that need to be modeled.
I don't think there are too many good solutions to that, except perhaps theorem provers from where you can also extract code from (e.g. Coq), but it seems either these tools are still difficult to use for engineers, or there is an expectation that models and actual implementations are going to be different anyway, making it difficult to see if the implementation actually implements the spec.
I also consider formal methods not testing. But model checking (e.g. with tlc) is something in between, and sort of takes advantage of the "This usually isn't feasible, but it's nice when it is.": when you limit your domain enough, it becomes feasible, yet exhaustively checking each small-world scenario gives a pretty good confidence on the model being correct.