An LLM-as-a-judge gives you another model's opinion; a logic solver gives you a proof. Here's how to check LLM answers and agent actions against a written policy, and get the broken rule named when one fails.
In October 2023, New York City launched MyCity, a chatbot to answer business owners' questions from thousands of pages of official guidance. Five months later, reporters at The Markup asked it whether a restaurant could stop taking cash. "Yes, you can make your restaurant cash-free," it replied. "There are no regulations in New York City that require businesses to accept cash as a form of payment." A local law had required exactly that since 2020.
Answers like that can carry legal weight. In 2024, a Canadian tribunal ruled that Air Canada was responsible for a refund its website chatbot had promised, contrary to the airline's own policy.
At Nearform, we build agents on today's stack of large language models (LLMs), retrieval and evals, and for most questions a well-tested agent is good enough. When an answer has to follow a written rule, there is a more rigorous option, and it is older than the models it checks. Symbolic AI, the branch of the field built on explicit logic, has checked statements against rules for decades. While deep learning drew attention in the 2010s, logic-based tools were verifying chip designs and flight software.
LLMs come from the other branch, the one that learns from examples. Can we pair that logic with an LLM, so that its answers are checked against the rules they are meant to follow? Translated into formal logic once, a written policy lets you check each LLM answer and agent action mathematically, and when one breaks a rule, the check names that rule and the values responsible.
Where symbolic AI went
The term “artificial intelligence” was coined in the proposal for a 1956 summer workshop at Dartmouth, and two of the approaches that followed matter here. Symbolic AI writes knowledge down as explicit rules over symbols, so every conclusion traces back to rules and variables that a person can inspect. Neural networks learn from examples instead, a line of research that goes back to Frank Rosenblatt's perceptron in 1958. They spent decades in the background, until a deep network from Geoffrey Hinton's group in Toronto won the ImageNet image recognition challenge by a wide margin in 2012. Today's LLMs are built on that approach.
Logic-based methods kept developing throughout, often outside anything labelled AI, in theorem provers, model checkers and solvers. A solver, the tool behind the examples below, takes a set of logical statements and works out whether they can all be true at once, returning either values that satisfy every one of them or a proof that no such values exist. Writing that logic took specialists, so formal verification was used where a mistake would cost more than they did. After Intel took a $475 million charge in 1994 for a division flaw in its Pentium processors, the industry's use of formal verification for floating-point hardware rose sharply, and in 2003 the Astrée static analyser proved that the flight control software of the Airbus A340 could raise no runtime error.
The clearest comparison between checked and unchecked code comes from a spacecraft. In 1997, a NASA team model-checked part of the Remote Agent, the autonomous software that later controlled the Deep Space 1 probe during a flight experiment, and found five errors. In 1999, while the Remote Agent was running the probe, a deadlock in a sibling subsystem that had not been checked stopped it, and the team reported that it was the same bug pattern as one it had found two years earlier.
What neurosymbolic AI is
Neurosymbolic AI is the name for systems that combine neural networks with symbolic reasoning. Researchers have worked on the idea for more than twenty years, and a 2020 paper called it the third wave of AI. The same year, Henry Kautz sorted the approaches into six types in a lecture at the annual conference of the Association for the Advancement of Artificial Intelligence. This article uses his Type 3 (written Neuro | Symbolic), in which a neural network and a symbolic system work on complementary tasks and interact through their inputs and outputs. The LLM writes the answer, and a solver decides whether it holds.
LLMs change who writes the logic, a job that used to take specialists. An LLM can draft rules from a policy document, the policy owner can review them clause by clause, and a solver can then check every later answer against those rules. Amazon Bedrock Guardrails has offered a managed version of that flow, called Automated Reasoning checks, since 2025.
How the check works
The check has three stages, shown in the diagram below, and only the first involves a person.
Rules are drafted and reviewed once per policy version, then every answer or agent action is checked against them.
Once per document version, an LLM translates the policy into named rules over a few typed variables, and the policy owner (or the subject-matter experts they assign, such as legal or compliance) reviews each rule next to the sentence it came from. Several translations of each sentence are compared, and test cases taken from the document catch translations that get a rule wrong.
For every answer, the LLM restates what it claims on the same variables.
The solver returns one of three verdicts:
valid: the answer follows from the rules, and the rules that prove it are named;
invalid: the answer contradicts a rule, and both the rule and the offending values come back;
satisfiable: the rules neither prove nor refute the answer, and the solver gives one example case where it holds and one where it fails, which shows the missing fact that would decide it.
If the facts themselves contradict the rules, there is nothing to judge, and the check reports them as inconsistent instead.
Satisfiable is the verdict a yes/no checker cannot express, and a common one in practice, because real questions leave facts out. Reporting it as either allowed or denied would be a guess, so the right response is to ask for the missing fact.
The more common way to check an answer today is LLM-as-a-judge, where a second model reads the answer and the policy and decides whether the answer complies. A 2023 study of judges rating chatbot answers found that GPT-4 agreed with human preferences over 80% of the time, about as often as people agree with each other. It also measured biases, such as favouring the first of two answers or the longer one. A judge can handle vague wording such as "reasonable", which logic cannot, but its verdict is another model output and can be wrong in the same ways as the answer it checks. The solver's verdict follows from rules the policy owner has reviewed, is the same every time for the same logic, and names the rules behind it, although it covers only what was translated into logic.
To see this in practice, let's build the check step by step.
Turning a policy into logic
Let's use a small travel policy as the running example. It has four sentences:
Trips exceeding EUR 1,000 require line-manager approval. All international travel requires line-manager approval. Employees may travel internationally once they have completed six months of service. No booking may be made before approval is recorded.
The examples use SMT (satisfiability modulo theories), which extends Boolean logic with theories such as integer arithmetic, so that rules can talk about amounts and durations. Its standard language, SMT-LIB, borrows its syntax from Lisp: every expression is a list in parentheses with the operator first. So (> costEur 1000) means costEur is greater than 1000, (and a b) means a and b, and (=> a b) means a implies b: whenever a is true, b must be true too.
Other approaches can express the same rules. Answer set programming with the clingo solver writes them in a Prolog-like syntax and suits policies built on defaults and exceptions, as well as search problems such as planning or product configuration, where the solver finds combinations that satisfy every rule. SMT suits an output guardrail, a check that runs on an answer before anyone sees it. The guardrail needs to know whether a claim follows from the rules, contradicts them or is left open, and an SMT solver answers that in two runs.
The solver we use is Z3. Microsoft Research presented it at a verification conference in 2008. It has been open source under the MIT licence since 2015. We install it with uv. The command uv tool install z3-solver puts the z3 command on your path, and the Python scripts later on declare Z3 as a dependency so that uv fetches it on first use. Here is a first run, with the cost sentence and one question:
declare-const creates a variable with a type, assert states something that has to be true, and check-sat asks whether the assertions can all hold together. The output, unsat (short for unsatisfiable), means they cannot: a EUR 2,500 trip without approval cannot be approved.
A Python if statement could encode this rule, and for one rule and one question it would be enough. Python is imperative: it runs your steps, in the order you wrote them, on the values you pass in. SMT-LIB is declarative: you state what must be true, and the solver works out whether any combination of values satisfies all of it, covering every case the rules allow rather than only the ones you happened to test. The difference grows with the policy. With dozens of interacting rules, nested if statements soon become hard to write correctly and harder to maintain, while a declarative policy stays a flat list of rules, each one added or changed on its own.
The whole policy fits in one file, policy.smt2:
(set-option:produce-unsat-cores true); report which named rules conflict; The facts a question can supply, and the outcomes the policy decides.(declare-const costEur Int)(declare-const international Bool)(declare-const managerApproved Bool)(declare-const tenureMonths Int)(declare-const tripApproved Bool)(declare-const bookingAllowed Bool); The situations the policy forbids, each defined once so the rules can reuse it.(define-fun expensiveUnapproved () Bool (and(> costEur 1000)(not managerApproved)))(define-fun abroadUnapproved () Bool (and international (not managerApproved)))(define-fun abroadTooSoon () Bool (and international (< tenureMonths 6))); The rules. (! ... :named x) gives each one a name the solver can report.(assert(!(=> expensiveUnapproved (not tripApproved)):named cost-rule))(assert(!(=> abroadUnapproved (not tripApproved)):named international-rule))(assert(!(=> abroadTooSoon (not tripApproved)):named six-months-rule))(assert(!(= bookingAllowed tripApproved):named booking-rule)); Not in the document: a trip that no rule forbids is approved.(assert(!(=>(not(or expensiveUnapproved abroadUnapproved abroadTooSoon)) tripApproved):named closed-world))
lisp
define-fun names a condition once so the rules can reuse it. Each rule stays a separate named assertion, so that when a trip is refused the solver can report which rule was responsible. The last rule is not in the document. The policy only lists the cases in which a trip is refused, so without this rule nothing could ever be approved. Approving every trip that no rule forbids is an instance of the closed-world assumption, and the policy owner has to confirm it.
Check the translation before any answer depends on it. The owner of this policy says that exactly six months of service qualifies. A translation that writes tenureMonths > 6 (strictly more than six, so six itself fails) gives the wrong rule. The solver still reasons correctly from it, so every verdict it returns is a correct proof about the wrong rule. Asking the solver where two translations disagree finds the problem:
Six is the only value where the two readings differ (distinct), and it is the boundary the sentence leaves ambiguous. When several translations exist, agreement works as a vote, and each disagreement becomes a question for the policy owner. Test cases find the same error independently: check the owner's answers for specific values (six months qualifies, five does not, twelve does) against each translation, and the > 6 version fails only the first. The solver has no way to tell whether the rules match the document, so that judgement stays with a person. An LLM-as-a-judge can help here, by flagging the rules that look different from their sentence, but the sign-off is the owner's.
Checking an answer
An employee in Hamburg asks whether they can book a EUR 2,500 trip to Berlin that has not been approved yet. We ask the LLM for the answer to the employee and, in the same response, for that answer as logic, with the facts and the conclusion kept apart:
Answer the employee in plain English. Then, between <smt> and </smt>,
restate your answer in SMT-LIB using only these variables:
costEur Int total trip cost in euros
international Bool the trip crosses a national border
managerApproved Bool a line manager has approved the trip
tenureMonths Int months of continuous service
tripApproved Bool the trip is approved under this policy
Write each fact the question gives you as a named assertion, such as
(assert (! (= costEur 2500) :named fact-cost)), and write what your answer
concludes as (define-fun claim () Bool ...). Assert nothing you were not told.
mdn
Suppose the model gets it wrong and says yes:
Yes, you can go ahead and book the EUR 2,500 Berlin trip.
<smt>
(assert (! (= costEur 2500) :named fact-cost))
(assert (! (not international) :named fact-domestic))
(assert (! (not managerApproved) :named fact-approval))
(define-fun claim () Bool tripApproved)
</smt>
mdn
One short Python script, verdict.py, turns that block into a verdict. It uses the Z3 Python library to ask whether the claim can be true and whether it can be false, and the two answers give the verdict. The # /// script block is inline script metadata, which uv reads to install Z3 before the first run. The flags on the first line keep uv quiet and make it use a prebuilt Z3 package instead of compiling one. After chmod +x verdict.py, it runs like any other command:
#!/usr/bin/env -S uv run --quiet --no-build --script# /// script# dependencies = ["z3-solver"]# ///# Usage: ./verdict.py policy.smt2 answer.smt2import re, sys
from pathlib import Path
from z3 import Solver, sat
defcheck(policy, answer, claim):"""Can the claim hold? Returns an example case, or the rules and facts against it.""" s = Solver() s.from_string(f"{policy}\n{answer}\n(assert (! {claim} :named checked))")if s.check()!= sat:returnFalse,sorted(str(c)for c in s.unsat_core()ifstr(c)!="checked") model = s.model() values ={str(d): model[d]for d in model} names = re.findall(r"\(declare-const (\w+)", policy)# the policy's variablesreturnTrue,{n: values[n]for n in names if n in values}defverdict(policy, answer): can_hold, if_true = check(policy, answer,"claim") can_fail, if_false = check(policy, answer,"(not claim)")if can_hold and can_fail:return"SATISFIABLE",f"the policy does not decide it\n holds when: {if_true}\n fails when: {if_false}"if can_hold:return"VALID",f"the policy proves it\n because of: {if_false}"if can_fail:return"INVALID",f"the policy rules it out\n because of: {if_true}"return"INCONSISTENT",f"the facts contradict the policy\n because of: {if_true}"if __name__ =="__main__": name, text = verdict(Path(sys.argv[1]).read_text(), Path(sys.argv[2]).read_text())print(f"{name}: {text}")
python
Save the part of the model's reply between the tags as answer.smt2 and run the check:
$ ./verdict.py policy.smt2 answer.smt2
INVALID: the policy rules it out
because of: ['cost-rule', 'fact-approval', 'fact-cost']
bash
The answer is invalid because of the cost rule and the two facts it applies to. Z3 calls this list the unsat core, a set of assertions that cannot all hold together with the claim, and it does not guarantee the smallest such set by default. You can show it to the employee or hand it back to the model to correct against.
Had a manager approved the trip, the model's block would differ in one line, and the same command proves the answer:
This time the policy proves the answer: the closed-world rule and the two facts leave no way to refuse the trip. Now take a EUR 2,000 international trip with approval, from someone whose length of service nobody mentioned:
The two example cases differ in one fact the question left out: at six months of service the trip is approved; at zero it is refused. Before answering, the assistant has to ask the employee for tenureMonths.
This example asks for the answer and its translation in a single call, which keeps it short. It also means that the model that wrote the answer translates it, and a model that misread the question will restate the facts it believed, so its logic fits the rules just as its answer did. In production, the translation is a separate step, as it is in the Amazon Bedrock Automated Reasoning checks mentioned earlier. A different model, or the same model with a different prompt, reads only the text and never sees the answering model's reasoning, which makes it much less likely that both get the same thing wrong. The facts come only from the user's question and the claim only from the answer, so the answer cannot add a fact nobody gave. The translator is told to assert only what the text states and to list anything it would have to assume, and each assumption becomes a missing fact that the check asks about.
Not every translation error does harm. A fact left out makes the claim satisfiable, and the check asks for it. The dangerous error is a fact nobody stated, such as an approval nobody gave, because it can make a wrong answer look proven. Evals measure how often that happens, with a set of questions whose facts are known, including some written to mislead: rewordings, negations, or an employee saying their manager has already agreed. The Nearform guide to building evals for reliable agents covers that work. The translation is measured rather than proven, and the verdict that follows from it is proven.
Checking an agent's actions
An output guardrail checks the facts as the model restated them, and nothing stops a model from asserting managerApproved without evidence. When an answer leads to an agent action, check the arguments of the tool call instead, because those are what will run. The policy then works as a precondition, a condition that has to hold before the call is allowed. The booking rule is already in the policy file.
Agent harnesses can run a command before each tool call. In Claude Code, this is a PreToolUsehook: it receives the call as JSON on standard input, and if it exits with code 2, the call is blocked and whatever it wrote to standard error becomes the blocking message. This hook, booking-hook.py, reads the call, turns its arguments into facts and passes them to the verdict() function from verdict.py, asking for bookingAllowed:
#!/usr/bin/env -S uv run --quiet --no-build --script# /// script# dependencies = ["z3-solver"]# ///# Runs before every book_trip call and allows it only if the policy proves bookingAllowed.# In production, read manager_approved from the approvals system, not from the call.import json, sys
from pathlib import Path
from verdict import verdict # verdict.py, in the same foldercall = json.load(sys.stdin)["tool_input"]facts =f"""
(assert (! (= costEur {call['cost_eur']}) :named arg-cost))
(assert (! (= international {json.dumps(call['international'])}) :named arg-international))
(assert (! (= managerApproved {json.dumps(call['manager_approved'])}) :named arg-approval))
(define-fun claim () Bool bookingAllowed)"""name, text = verdict((Path(__file__).parent /"policy.smt2").read_text(), facts)if name !="VALID":print(f"{name}: {text}",file=sys.stderr)# becomes the blocking message sys.exit(2)# exit code 2 blocks the tool call
python
It is registered in the project's .claude/settings.json and, like verdict.py, needs chmod +x. Here book_trip is served by a Model Context Protocol (MCP) server called travel, which is why Claude Code names the tool mcp__travel__book_trip:
Any exit code other than 2 lets the call through, so the || exit 2 after the command makes a crash, or a missing uv, block the booking too.
An unapproved EUR 2,500 booking never reaches the travel system:
$ echo'{"tool_input": {"cost_eur": 2500, "international": false, "manager_approved": false}}'| ./booking-hook.py
INVALID: the policy rules it out
because of: ['arg-approval', 'arg-cost', 'booking-rule', 'cost-rule']$ echo$?2
bash
A precondition is only as sound as the code that binds its values, which is why the comment in the hook says to read manager_approved from the approvals system. The environment the call runs in needs controlling too. A container limits what an allowed call can reach but cannot stop one that breaks the policy, and the Nearform write-up on securing agentic workflows with containers covers that side.
Where it fits
The approach fits wherever an answer has to follow a written rule that can be stated in concrete variables. Lending is the clearest case. Age, income, deposit and term are numbers, lenders already document their rules, and the European Union's AI Act classifies AI systems that evaluate the creditworthiness of individuals as high-risk. Clinical trial protocols are another, since eligibility criteria, dosage limits and required steps are set out before the trial starts. The everyday case is an internal assistant for human resources (HR) policy, answering questions about leave, expenses or benefits, with each answer checked against the policy before the employee sees it.
Where it stops
Five limits are worth knowing before you start.
Logic has a narrow scope. It covers amounts, dates, categories and workflow steps, not tone or subjective judgement. A policy written around words like "reasonable" will either resist translation or be translated into something more precise than the document says.
The solver can fail to decide. With rules that multiply two variables, Z3 can answer unknown instead of sat or unsat. verdict.py counts that as impossible, so a production check should report it separately, as a failed check rather than a verdict.
A satisfiable verdict is not permission. It is weaker than a proof, and treating it as approval discards the only guarantee the check offers.
A policy made only of prohibitions can never prove a yes. Remove the closed-world rule from the policy file and the approved trip above comes back satisfiable instead of valid.
Every check has a cost. The model writes a few extra lines of logic with each answer, and the solver runs twice. Translating and reviewing the policy is a one-off cost for each version of the document. The extra step is easy to justify on a lending decision, less so on a chatbot reply that carries no compliance risk.
Back to the initial error
The rule MyCity got wrong is a specific section of the city's Administrative Code, and it translates into a single assertion. The file below is simplified: the law also defines which businesses count, and a real translation would include those details and be reviewed by the city's lawyers.
(set-option :produce-unsat-cores true)
(declare-const foodOrRetail Bool) ; the business is a food store or retail establishment
(declare-const paidOnPremises Bool) ; the customer pays on the premises
(declare-const mustAcceptCash Bool) ; the law requires the business to accept cash
; NYC Administrative Code § 20-840, simplified: food stores and retail
; establishments must accept cash for payments made on the premises.
(assert (! (= mustAcceptCash (and foodOrRetail paidOnPremises)) :named cash-rule))
mdn
The chatbot's answer, translated the same way as the travel answers, says the business is a restaurant, its customers pay on the premises, and it does not have to accept cash:
$ cat mycity.smt2
(assert (! foodOrRetail :named fact-restaurant))(assert (! paidOnPremises :named fact-pays-at-table))(define-fun claim () Bool (not mustAcceptCash))$ ./verdict.py cash-law.smt2 mycity.smt2
INVALID: the policy rules it out
because of: ['cash-rule', 'fact-pays-at-table', 'fact-restaurant']
bash
The cash rule and the two facts that trigger it rule the chatbot's answer out, and that list is what a restaurant owner needed to see. The chatbot's other wrong answers reported by The Markup, about taking workers' tips and refusing housing vouchers, were about written rules too, and each could be checked like this one.
What a proof adds
Teams already have ways to improve LLM answers. Evals measure how often an agent is right across a dataset, and the Nearform guide to building evals for reliable agents covers that work. Prompt techniques make a model more likely to follow a rule, as in the Nearform post on re-anchoring agent safety with a Mastra processor. An LLM-as-a-judge can quote the rule it thinks was broken and explain its reasoning. A policy expressed as logic adds a verdict to each individual answer, with a proof whenever the answer is valid or invalid. For an invalid answer, it shows that no case allowed by the rules makes the answer true, then identifies the rule and values that exclude it. A compliance reviewer gets a record to check without trusting the model.
To try it on one of your own policies:
pick a document with concrete variables and a named owner, such as an expenses policy or a set of mortgage eligibility criteria;
have an LLM translate a few of its sentences into SMT-LIB, and ask the owner to compare each rule with its source sentence;
write test cases from the document's own boundaries before the rules go into use;
put a verdict script like the one above in front of one LLM answer or one agent action, and send every satisfiable verdict back to the user as a question.
If you're planning to take a check like this into production, Nearform can help you set up the project and the review process from the start, drawing on our experience in AI-native engineering, so that the answers your agents give are ones you can prove.
But wait - there's more.
Nearform publishes real-world learnings on data & AI, engineering, and digital strategy - with more merged in weekly.
Insights
Perspectives on AI in engineering, product development, and strategy, for enterprise executives.
Rules are drafted and reviewed once per policy version, then every answer or agent action is checked against them.
