> your specifications can and usually does have bugs

One cool thing about formal verification is that you can not only prove things about your code, but you can prove things about the specification itself (with some approaches, at least). This includes proving arbitrary properties, proving the presence of bugs, proving the absence of bugs and in some cases, even proving full correctness of the specification.

> I'm bullish on more sophisticated type systems [...] but not formal verification.

I don't know what kind of formal verification framework you used that left you with this conclusion, but the more sophisticated is your type system, the closer you are to doing formal verification.