Comment by soist

How do they verify the output preserves semantics of the input?