[zozbot234]

Full program inference from specs is actually a very hard problem, because the compiler/SAT solver cannot autonomously derive loop invariants (or, similarly, inductive hypotheses) that are necessary to write correct code. So using a LLM that can look at the spec and provide a heuristic solution makes a lot of sense. Obviously the solution still has to be verified, though.