> Now you have to somehow write down what all that does.

I think the core difficulty is that there's no way to know whether your spec is complete. The only automatic feedback you can hope to get is that, if you add too many constraints, the prover can find a contradiction between them. But that's all (that I'm aware of, at least).

Let's take an extremely simple example: Proving that a sort algorithm works correctly. You think, "Aha! The spec should require that every element of the resulting list is >= the previous element!", and you're right -- but you are not yet done, because a "sorting algorithm" that merely returns an empty list also satisfies this spec.

Suppose you realise this, and think: "Aha! The output list must also be the same size as the input list!" And again, you're right, but you're still not done, because a "sorting algorithm" that simply returns inputSize copies of the number 42 also satisfies this new spec.

Suppose you notice this too, and think: "Aha! Every element in the input should also appear the same number of times in the output!" You're right -- and now, finally, your spec is actually complete. But you have no way to know that, so you will likely continue to wonder if there is some additional constraint out there that you haven't thought of yet... And this is all for one of the tidiest, most well-specified problems you could hope to encounter.

Major flaws in a specification for one function are usually quickly picked up when the proof for another function relies on the missing specification properties e.g. if you only prove the list returned by a function has a certain length and nothing about the contents of the list, you're going to quickly find out when another function needs to prove anything trivial about the contents of that list.

Not that it's flawless either, but supplementing with standard e.g. unit tests helps catch specification bugs like this and you could generate unit test examples from the specification to review for correctness as well. You would notice problems when running the program too just like with regular programming, you wouldn't just write proofs about your program and not try running it.

Nothing is perfect but just like in regular programming languages where adding a few simple regular automated tests or some more accurate static type annotations (e.g. JavaScript to TypeScript) will catch a lot of problems compared to nothing at all (and with diminishing returns), a proof of some simple properties will flush out a lot of bugs and edge cases. So I feel the common reaction of "specifications can have flaws" is overplayed when it's clearly a big step up the process of eliminating bugs.

Does an alternative exist that's foolproof?

Producing positive and negative examples is exactly where model checkers shine. I always write "falsy" invariants to produce examples of the specification reaching interesting control states for at least one input. After that, I think about the system boundaries and where it should break. Then, the model checker shows that it indeed breaks there.

Having a specification does not mean that one should not touch it. It is just a different level of experimental thinking.

I think you're right, but technically too many constraints doesn't mean the spec is wrong: some may be redundant, and that can be ok or even helpful. A lack of contradictions doesn't mean it's right either. I would argue that the problem of not knowing you got all the constraints specified is the same as not knowing if all generic requirements are specified. It's more work to formally specify anything and the constraints are more difficult to casually interpret, but in either case doneness is more of a continuum than a binary attribute.

And ... so what? Nobody ever said specs are error free or complete. Heck, you didn't even get into liveness, dead lock issues.

The salient question: is risk reduced for the time alotted to write a spec in say spin or tla+?

Formal specs are risk reduction not magic.