Well, that's true for simple type systems. Dependent types are not so practically usable. You're absolutely right that simple types prove some "simple" properties, but we know what characterises them: they're inductive (or composable) invariants, i.e. P(a ∘ b) ⇔ P(a) ∧ P(b), for some program composition operator ∘ (I'm papering over some important but nuanced details). It's just that most program correctness properties we're interested in are not inductive, so the "proving power" of simple types is not strong (another way of describing it is that it's not powerful enough to express propositions with interleaved universal and existential quantifiers).

So when we talk about formal methods, we're usually interested in those that can express and/or "verify" (to some degree of confidence), non-composable properties and propositions that involve interleaved quantifiers.