>> Proving correctness is crucial in large systems.
You can't do that...
The model checker says the specification satisfies the properties you wrote within the finite state space you explored...
You can write proofs in TLA+ and many other formalisms. You don’t need to ever use a model checker. The proofs hold for an infinite number of infinite-length executions. We are definitely not limited to finite behaviors.