You don't need a full correctness checker to get a useful product though. New code generated by the current generation of LLMs, which also compiles and passes existing tests, is likely to be somewhat useful in my experience. The problem is that we still get too much code that doesn't pass these basic requirements.
Our notion of "correct" for most things is basically derived from a very long training run on reality with the loss function being for how long a gene propagated.