SMT verifier
Check one answer or run the example suite against Z3.
Fixed grammar · bounded solver · no LLM calls
01
Verification input
Problem
Loading constraints…
Loading service limits…
Advanced JSON & example notes
Problem JSON
Candidate JSON
Example note
Synthetic inputs only. Verification concerns the supplied mathematical encoding, not a natural-language interpretation.
02
Verification report
Loading examples…
No verification yet
Choose an example and check its assignment. Evidence appears only after a solver response.
No suite has run.
Each case makes a real, sequential verification request. “Matched” means the returned outcome matches that bundled example’s expected code; it is not a general benchmark result.
Up to six completed runs, kept in memory. Reloading or leaving clears the history. Nothing is saved to browser storage.