Some things like abstract interpretation scale quite well.

The Airbus fly-by-wire code (~100 KLOC) can be statically verified in about an hour with a modern PC.

This is not a formal proof, but it excludes entire classes of runtime errors such as de-referencing a null pointer.