This is a weekend hack that I'd like to further develop as it's working surprisingly well.
Using MCTS, we can explore a space of possible verified programs with an LLM. We check the partial programs at each step, and so steer towards programs that pass the verifier.