[dgacmu]

Not really. Imagine the proof says: "in this protocol, when there are more than 0 participants, exactly one participant holds the lock at any time"

It might be wrong, but it's pretty easy to inspect and has a much higher chance of being right than your code does.

You then use proof refinement to eventually link this very high level statement down to the code implementing it.

That's the vision, at least, and it's sometimes possible to achieve it. See, for example, Ironfleet: https://www.microsoft.com/en-us/research/publication/ironfle...