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.
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.