A formal specification language doesn't have to be deterministic.

And yes, if you can prove that the implementation is correct with respect to the formal spec, you are good, and it doesn't really matter how you got the implementation.

Refinement is one approach, personally, I just do interactive theorem proving.