I still see your point but quoting the How Amazon Web Services Uses Formal Methods paper:

  In each, TLA+ has added significant value,
  either finding subtle bugs we are sure
  we would not have found by other means,
  or giving us enough understanding and
  confidence to make aggressive performance
  optimizations without sacrificing correctness.

Type checking, borrow checking and unit testing are similar albeit weaker tools that allow rapid development by providing a safety net.

I'm on the "yes type checking" side of the perennial "which is more efficient" programming language debate, but when we talk about "formal methods" in the context of eradicating security vulnerabilities, the subtext is "formally proving correctness", not simply any tool that increases rigor. I agree, boringly, that there are PL tools that apply rigor to increase development speed.

The belief that software could be affordably proven correct was pervasive in the 70s, it led to a research winter, and now formal methods is very much about adding rigor and catching more bugs (some of the most promising directions in contemporary formal methods research revolve around reducing soundness to help find more bugs more quickly).

There is a small subdiscipline of formal methods that comes from programming language theory (judging by conferences, it makes up no more than 10-20%) that does still have this 1970s "subtext", but actual researchers or practitioners are usually careful with what they actually say, and you'll most often find such claims explicitly made only by fans.

I see your point.