You can use an external proving mechanism and feed the results to the LLM. A sufficiently rich type system (think Idris rather than C) or a sufficiently powerf

You can use an external proving mechanism and feed the results to the LLM. A sufficiently rich type system (think Idris rather than C) or a sufficiently powerful test suite (eg property-based tests) should do the trick.