You seem a bit confused?

First, the halting problem is only undecidable on arbitrary programs. Here we would be writing programs specifically to be easy to prove correct. In fact, we would be developing programs and proof at the same time.

Second, determinism is a nice property, but it's independent of whether you can proof software correct.

Have a look at eg randomised quicksort or the 'expected linear time minimum-spanning-tree algorithm' https://en.wikipedia.org/wiki/Expected_linear_time_MST_algor...

Or have a look at HyperLogLog. https://en.wikipedia.org/wiki/HyperLogLog

HyperLogLog only gives you a probabilistic approximation of the true number of distinct items. Here the proof would be about the probability that you are within some acceptable window around the true answer.