That's not enough for proof purposes. It allows you to build a test that deterministically tests one path, but it does not give you control over all possible tests.
In fact I seem to be a bit iconoclastic on this matter but I'm not even a fan for testing purposes. Even non-proof-based testing needs the ability to test that goroutines may execute out of order. Nothing prevents a goroutine scheduled for 2ms from now to run all the way to completion before a goroutine scheduled to run 1ms from now even starts, but AFAIK this approach doesn't let you test that case. Such logic is not valid in a multithreaded system; it is at most the most likely progression, not the only possible progression.
But since we live in the world where the question is more will anyone write a concurrency test at all, moaning about not having a perfect one is missing the point, I suppose. I won't deny a deterministic test is better than a non-deterministic test in general.
There may be more there than meets the eye at first glance.
I'm not saying this easy to do at the moment, but the possibility is there.
If you can take control of all timers/sleep in your Go program, then you have, in effect, complete control of Goroutine scheduling.
If you assign a distinct time point to each goroutine, say based on its ID, and then have the goroutine sleep until that point, then you have also assigned the order in which those goroutines will run. Each will "wake up" alone, only at the next point at which the clock is forced to advance--which is when the previous goroutine blocked.