Neurosymbolic guardrails for AI agents: answers you can prove Nearform engineers argue that pairing large language models with symbolic AI solvers can mathematically verify agent answers against written rules, citing New York City's MyCity chatbot, launched in October 2023, which told businesses they could go cash-free despite a local law requiring cash acceptance since 2020, and a 2024 Canadian tribunal ruling that held Air Canada liable for a refund its website chatbot had promised. The authors trace the approach to decades of formal verification, including NASA's 1997 model-checking of the Remote Agent software that found five errors before an unchecked sibling subsystem deadlocked during the 1999 Deep Space 1 flight experiment, and Intel's $475 million charge in 1994 over the Pentium division flaw. 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 https://themarkup.org/artificial-intelligence/2024/03/29/nycs-ai-chatbot-tells-businesses-to-break-the-law 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 https://www.americanbar.org/groups/business law/resources/business-law-today/2024-february/bc-tribunal-confirms-companies-remain-liable-information-provided-ai-chatbot/ 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 https://en.wikipedia.org/wiki/Symbolic artificial intelligence , 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 https://ojs.aaai.org/aimagazine/index.php/aimagazine/article/view/1904 , 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 https://arxiv.org/abs/1409.0575 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 https://en.wikipedia.org/wiki/Pentium FDIV bug in its Pentium processors, the industry's use of formal verification for floating-point hardware rose sharply, and in 2003 the Astrée https://www.astree.ens.fr/ 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 https://ntrs.nasa.gov/api/citations/20000055731/downloads/20000055731.pdf 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 https://arxiv.org/abs/2012.05876 . The same year, Henry Kautz sorted the approaches into six types in a lecture https://onlinelibrary.wiley.com/doi/10.1002/aaai.12036 at the annual conference of the Association for the Advancement of Artificial Intelligence https://aaai.org/about-aaai/ . This article uses his Type 3 https://en.wikipedia.org/wiki/Neuro-symbolic AI :~:text=Neural%20%7C%20Symbolic 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 https://docs.aws.amazon.com/bedrock/latest/userguide/guardrails-automated-reasoning-checks.html , 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. 1. 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. 2. For every answer, the LLM restates what it claims on the same variables. 3. 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 https://arxiv.org/abs/2306.05685 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 https://smt-lib.org/ , 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 https://en.wikipedia.org/wiki/Answer set programming with the clingo https://potassco.org/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 https://github.com/Z3Prover/z3 . Microsoft Research presented it https://link.springer.com/chapter/10.1007/978-3-540-78800-3 24 at a verification conference in 2008. It has been open source under the MIT licence since 2015. We install it with uv https://docs.astral.sh/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: js $ z3 -in <<'EOF' declare-const costEur Int declare-const managerApproved Bool declare-const tripApproved Bool assert = and costEur 1000 not managerApproved not tripApproved assert = costEur 2500 assert not managerApproved assert tripApproved check-sat EOF unsat 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 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 https://en.wikipedia.org/wiki/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: js $ z3 -in <<'EOF' declare-const tenureMonths Int assert = tenureMonths 0 assert distinct = tenureMonths 6 tenureMonths 6 check-sat get-value tenureMonths EOF sat tenureMonths 6 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