Full verification is one, but that is still challenging at scale. Formal methods has many weaker methods as well which are easier to apply in general (automated

Full verification is one, but that is still challenging at scale. Formal methods has many weaker methods as well which are easier to apply in general (automated proof, abstract interpretation, static or dynamic model checking, hell some would even argue the judicious use of dynamic checks is a kind of formal methods). I think that a shift from "this is my program, it's a sequence if steps that does what it does" to "I asked a LLM to generate me a program that does this vague thing I want" makes you naturally ask questions like "wait is it actually doing the thing I want" and "what do I even want it do do". Formal methods, broadly, has a lot of good answers to those questions.