An OpenAI-compatible bridge that anchors LLM reasoning in logical reality by using Z3 to incrementally verify, self-correct, and prove the uniqueness of SMT-encoded solutions.