Would formal verification work for a more involved, "entreprise-level", code bases?

Also I imagine it would be fairly hard to verify code that depends on external state (e.g. reads from a DB).