The problem I've been having is the LLM's are super dodgy, not even ten minutes ago the 'solution' to a proof failing was to disable that check in the static analysis harness so the tests pass since their first try (with a counter example and lemma from the literature in hand) didn't fix the issue.

Maybe it's an issue because it controls both sides of the fence and can change things willy-nilly when it thinks I'm just watching the youtubes but I haven't been able to find a another way to do this so, here we are...