Typical proofs don’t cover side channels, just ISA semantics. With the big asterisk that most programs are running on top of an unverified kernel on an unverified machine-level blob on an unverified ISA implemented by an unverified chip, you can absolutely prove the behavior of programs. Lamport has an unusual attitude towards verification and comes towards it from a slightly different angle, and model checking is not a good approach to machine-level proofs.