I think how to verify real compiler optimisations is still an open research question. Does any other compiler do it formally? I'm not sure it's reasonable to expect Go to do it.
In the general case, it's definitely not solved. Java and C/C++ (gcc) are known to have had compiler optimizations introduce bugs. (I assume the same is true about clang and other compilers; I just happen to remember about these ones).
For a recent Java one with Hotspot JIT, there is this FOSDEM 2017 talk.
"....Escape Analysis and Intrinsics, two commonly used HotSpot optimization techniques. I'll show how a combination of these two features can optimize away IndexOutOfBoundsExceptions in some corner cases where they are required by the standard..."
