A language model proposes an answer to a constraint problem. Z3 either certifies it or returns the exact constraints it breaks. Verification runs here, live, in milliseconds.
Verifier code from llm-smt-verifiable-reasoning · the model-generation half is not exposed here (it costs money per call) · problems from the repo's 500-problem linear-arithmetic set.