I do not work on verification directly, so I do not know the details. I believe at a high level you generally have a automated first pass which generates a sour

I do not work on verification directly, so I do not know the details. I believe at a high level you generally have a automated first pass which generates a source<->machine trace. You then have multiple independent reviews validating the correctness and exhaustiveness of the trace. Generally in these environments you build with optimizations off unless needed to ease this validation process as, obviously, you must validate the released/deployed version.