CompCert produces surprisingly fast native code.

This 2022 article [0] says it generates binaries that run about 7% slower than what GCC produces with -O1.

[0] https://www.cs.cornell.edu/courses/cs6120/2022sp/blog/compce...