SMT Solver

An SMT solver takes a bunch of rules and conditions all at once and mathematically works out whether they can all be satisfied without contradiction. Think of it less like solving a complex Sudoku puzzle by hand, piece by piece, and more like a calculator you feed the whole rule set into, which then tells you flatly whether it's solvable or not.

Say a service wants to check whether "this answer is allowed for this question." First, the question and answer are converted into logical formulas and slotted into the policy's rule variables. Then the SMT solver compares this formula against the policy rules to determine whether it holds. This isn't a probabilistic guess along the lines of "this looks plausible because I've seen lots of similar cases before" — it works like a mathematical proof, where if the conditions are met, the result is guaranteed to be correct too, so the basis for the judgment is clear.

These verification tools typically take rules written in a standard input format called SMT-LIB, which can be thought of as a kind of formal language shared across many automated proving programs.

The article explains that "an SMT (Satisfiability Modulo Theories) solver compares this logic against the policy rules to verify and render a judgment." The key point here is that the SMT solver isn't a tool that lets AI guess at an answer roughly — it's a separate verification engine that mathematically confirms whether a logical formula contradicts the rules. The AI (foundation model) only translates the question and answer into logical formulas; the actual true/false determination is handled by the SMT solver.