you can do those things under the assumption "the compiler is correct". That still very much counts as formal verification.