program synthesis is a research area that combines searching over program spaces with formal verification. sometimes these are separated, other times we can get an SMT solver to help with the search, as well as doing the verification part.

in any case, it's hard to overstate how cooked the searching part is, due to LLMs. they're just incredibly good at it, and this is nice because our previous solutions were not particularly impressive.

so far LLMs haven't changed the verification part at all