I'm sure lots of people have been thinking/working along that direction. I think the idea of combining LLMs with formal verification/proof assistant tools (Lean, Coq, Isabelle,...) is particularly interesting. Anyone is aware of any major groups working on open source solutions for this?