Comment by HelloNurse

Focus on formal verification is a technique to "harden" an unreliable LLM that produces meaningless slop from arbitrary text into a compiler that produces a correct program from a concise, formal input.

"Writing formal specs" means simply programming, taking a step upward in programming language abstraction level, and whether it's going to be easy remains to be seen.