I'm assuming you're referring to formally proven programs. If that's the case, do you have any pointers?

Aside from the trivial while(!transactionSucceeded){retry()} loop, I have trouble proving the correctness of my programs when the number of threads is not small and finite.

This is true. However, the blast radius may be smaller with a process model. Also recovering from a fatal error in one session could possibly be easier. I say this as a 30-year threading proponent.

I think the point is that some mistakes in process based code are not realized as the bugs that they will be in threaded code?

It can be. Anything can be. It is far more treacherous, though.

In theory, yes. In practice, no.

It is just harder.