Check out Frama-C/Alt-Ergo/Why3 projects. They address this directly. I think I'm oversimplifying it, but as I understand they write the entire prover as a pro

Check out Frama-C/Alt-Ergo/Why3 projects. They address this directly. I think I'm oversimplifying it, but as I understand they write the entire prover as a proof theorum itself, then use an alternative prover to prove the original theorum, then they write the program and use the proofs to proof itself. Lots of good academia surrounding that portion of it. Further, assuming I'm reading your implication correctly, languages like Go, Rust or Zig do NOT have formal verification properties to them. They definitely have some neat anti-footgun tools, but they are very far away from formally specified code.