Which you can provide on your Markdown files as well.
These are not what-ifs, this is an active area of research currently,
"CGO 2022 Keynote: Compiler 2.0"
https://www.youtube.com/watch?v=w_sX9aZoZxg
"Machine-Generated, Machine-Checked Proofs for a Verified Compiler"