prince617··on Verified Code Transpilation with LLMsThe paper states that they iterate multiple times with the LLM and only take answers that don't contain hallucinations and can pass the proof engine.
prince617··on Froid: Optimization of Imperative Programs in a Relational Database [pdf]You might want to check out this related work: http://casper.uwplse.org