The biggest win of predicate-based formal verification (or really any formal verification at all) is forcing you to carefully think about invariants and properties of your code (independently of whether you can prove them). Even if you can't prove them, these serve as useful formal documentation for maintenance purposes and help guide and maximize the efficiency of other techniques such as traditional testing. If you can characterize your code with useful invariants and properties, then you can write useful unit tests and property tests, rather than writing happy path tests that fail to actually catch many bugs.

Assertions are one piece of the puzzle, but often times you want to reason about how something fits in a larger context (the canonical example of this is something like the associativity of an operator, which isn't something you can check for with an assert statement within the operator), which is where independent predicates come in handy.

In general, I think of fuzzing and property-based testing as a lightweight and practical stand-in for the verification part of formal verification. If your formal properties can be proved quickly (e.g. by a short manual proof or some sort of automated engine) then great! If they can't, you can still often times convert it into a fuzzing-friendly format or a property test and get a fairly high degree of confidence of correctness that way.

Because they work at different levels and provide different strengths.

Model-checking a TLA+ spec is fully automatic, but the specification is probably at a high level; fuzzing can find low-level implementation problems.

SPARK or languages/tools like it specifies at the code level, but verifying at the same level as fuzzer can be very laborious if at all feasible (same as using the proof assistant with TLA+).

In short, software verfication comes with huge tradeoffs among labor, soundness and scale. There is no one solution that subsumes the others.

> why not just use a logic programming language or something like SPARK/TLA+ anyway?

This (usually) requires a comprehensive reference model of your design whereas asserts can be added very adhoc and phased in as appropriate.

Also, fuzzing doesn't require assertions, it just yields more/better fruit that way.

Wouldn't it require a set of business rules instead of a comprehensive design model? It's logic programming. Based on those rules it can determine whether the input I passed in should produce the output I received.

The logic programming suggestion would be much less work but is usually overlooked. Probably because that kind of subtle, concise code is the polar opposite of brute force fuzzing.

> Wouldn't it require a set of business rules instead of a comprehensive design model?

Well, I was imagining something like a library being tested/verified rather than an application or system. But either way, you have to model the features of the code-being-verified and the model must be comprehensive. An incomplete reference model usually will result in false defects.

It's a lot easier to sprinkle some assertions throughout an existing legacy application than it is to reimplement that application in something like TLA+

>Felt much easier to insert my thots into the source.

thots -> thoughts?