The non-determinism is one of the relevant features of this layer of abstraction! And one can learn to validate that the translation is being done properly. Some of the tools you have include writing extremely detailed specs, generating visualizations of the internals of the tool, or (perhaps) reading the code, though that becomes less feasible with volume.

Basically it turns out that code is full of incidental details and what you really want is to verify the important parts, while receiving a guarantee that the vast tail of incidentals is handled "reasonably."