Practical Neurosymbolic AI Is Here

This is the fourth post in a series introducing SMEme (pronounced 'smee-mee'). SMEme lets you author a decision procedure in language you can read and edit, then a symbolic constraint solver (System 2 AI), not the model, computes what follows. SMEme Core is source-available under a Sustainable Use License inspired by n8n, so you can self-host. The architecture post laid out the neurosymbolic architecture: models propose, people authorize, and formal reasoning determines what follows. The introduction showed it in a legal decision-support workflow. The oil-shock post showed what a decision procedure adds once research is automated. Here I wire SMEme to TypeSafe's new System One model, Jev, inside a LangGraph harness.

Space Coast, FL — TypeSafe's manifesto frames their goal as the neurosymbolic dream of "neural networks for perception paired with symbolic logic for reasoning," which they summarize, cheekily, as "smart if-statements." In their vision, the symbolic half is the code you write around Jev. Ordinary program logic is symbolic computation, but it isn't what is usually meant by symbolic AI. SMEme is symbolic AI in the classic sense, an explicit formal theory and a solver that reasons over it. It is the System 2 component of the neurosymbolic architecture. Our architecture post laid out a SMEme + (traditional) LLM neurosymbolic architecture in a LangGraph harness two weeks before Jev launched. In this post I'll show how to add Jev to the harness, highlighting its use as TypeSafe's Harness Engineering layer: a Choice over authorized options, search and retrieval of the state a later judgment will see, verification of an agent's judgment against the gathered state (Jev-as-judge), confidence-gated routing into SMEme's reasoning pipeline or human interrupt, and speculative fan-out so the System 2 component (SMEme), not the model, logically infers what answers matter.

The next few sections explain why the reasoning layer is separate from the model, and why that matters when a decision has to be defended. You can skip to the code.

SMEme is Symbolic AI (the System 2 reasoning layer), not just 'deterministic code'

TypeSafe's manifesto makes the case that people only build on components they can inspect, test, and constrain piece by piece. In most harnesses the decision procedure is the most deeply buried dependency and the least inspectable one. Their how-to says if a question would hide several judgments, decompose it. Ask each factor as a separate atomic question, then combine the results in code. Their primitives guide repeats the instruction. When a judgment needs more than a single one-shot classification or choice, or depends on several independent factors, ask each separately "and combine the answers with your own logic."

SMEme is that combining logic, authored by the expert and reasoned over by a solver. It isn't a decision-tree runner or a pile of deterministic branches. The tree is the authoring surface, a knowledge artifact the user can read, challenge, and authorize without being a knowledge engineer. Deploy compiles it into a frozen representation, and every evaluation hands the resulting propositional theory to Z3, a symbolic constraint solver. The solver doesn't walk a path. It reasons over the whole decision procedure at once, under incomplete information. It can tell you that a conclusion is forced no matter how the open questions come back, that two outcomes are still live and exactly one question separates them, or that the admitted answers can't all be true. It can tell you which answers did the work, what would have to change to reach a different outcome, and which unanswered question is still worth anyone's time. A branch runner doesn't do any of that. A solver over a formal theory can.

That's what earns the System 2 label. Not slower thinking, but deciding where attention goes and what the committed answers entail.

It's the same division of labor behind DeepMind's AlphaGeometry, where a language model proposes geometric constructions and a symbolic deduction engine derives what follows from them. It may be overengineering for ticket triage. But for expert decision support, or wherever robust logical analysis is needed (legal, medical, military, policy, underwriting, etc.), SMEme delivers that System 2 component as an MCP tool set, with no knowledge engineering, ontologies, or specialized user training.

Two primitives, one boundary

Jev takes state and typed questions and returns typed answers with probabilities. Choice picks from a set of options and returns per-option probabilities plus a confidence score. Score rates against ordered levels. Noul answers yes or no as a probability. Every question in a request is answered in one parallel pass, and TypeSafe says most queries complete in about 100 milliseconds.

SMEme takes a decision tree an expert writes in natural language, made of questions with finite allowed answers, branching conditions, and conclusions. When the expert Deploys it, SMEme compiles it into a frozen intermediate representation (IR). Every evaluation encodes that IR into a propositional theory for the solver. At runtime, SMEme's Inquire loop takes the evidence admitted so far and returns the next unanswered question that can still change the outcome, as a blind task with an id, a stem, and the allowed options. Once the case resolves, it returns a report instead.

When put side by side, the Jev + SMEme integration nearly writes itself:

That's the whole adapter. SMEme already emits the kind of object Jev was built to consume.

This works because SMEme's questions aren't prompts. They are the vocabulary of the decision procedure. Each question and its allowed answers define propositions the theory reasons over. Jev, an LLM, or a person can determine which authorized answer best fits the evidence. Jev can't invent a new answer by design, since it only returns one of the options it's handed. SMEme is what makes those options the ones the expert authorized, and it rejects anything else, whoever proposed it. None of them decides what admitting that answer entails under the procedure.

To Jev, the question is the prompt and the state is the context. Its weights induce a distribution over the authorized answers, and the judgment is which answer best fits the case. That is bounded classification, not open-ended generation. In the architecture post I left all of that to an LLM. Now a dedicated component can take the state an LLM assembled and return structured answers over a natural-language vocabulary the expert authorized. Once admitted, those answers are the native inputs to SMEme's System 2 reasoning. Practical neurosymbolic AI is here.

The harness

SMEme's AI-assisted decision tree authoring is built on LangGraph. This is the same stack on the other side of the loop.

                        LangGraph
            state · routing · retries · interrupts
                            │
                            ▼
                    SMEme Inquire
         "here is the next question that can
          still change the outcome"
                            │
          ┌─────────────────┼─────────────────┐
          ▼                 ▼                 ▼
         Jev            LLM agent          SQL / code
   bounded judgment   retrieval, tools,   exact lookup,
   over given state   multi-doc work      dates, counts
          │                 │                 │
          └────────┬────────┴─────────────────┘
                   ▼
            proposed answer
      + confidence + evidence provenance
                   │
                   ▼
      admission: case commitment (harness policy)
    auto-admit above threshold, or a person
     accepts / changes / abstains
                   │
                   ▼
           SMEme recomputes
     T(IR) ∧ E ∧ A  →  next question (loop) or report

(Jev unsure or none fit → agent; agent's evidence → Jev judges blind)

The division of authority is the point:

Expert      → the procedure (rule commitment)
LangGraph   → what runs
Jev         → fast judgment over supplied state; independent re-answer to check an agent's choice
LLM agent   → open-ended investigation
SQL / code  → exact computation
Admission   → case commitment (a person, or the operator's threshold)
SMEme       → what follows

LangGraph controls what runs. SMEme controls what follows.

Jev doesn't gather evidence. It knows only the state it's handed, and it can't search, query, or read beyond it. So every Jev judgment sits downstream of something that assembled that state. Their use-case map puts Jev inside that gather workflow but only to score and rank candidates already in hand and select the context a later judgment will see. A question's path can be Jev retrieving and Jev judging. Gathering and proposing are still separate jobs, and each question can pair them differently.

The traditional reasoning LLM is still the one you want when the job is finding the context a question needs — writing queries, reading across sources, synthesizing a bundle. That is generative retrieval, and Jev isn't designed to do that. On those questions the LLM will usually have already picked an option while assembling the state. Keep that conclusion out of what Jev sees, or Jev is scoring the agent's write-up instead of independently judging the evidence. Jev then answers the same blind question from the gathered state alone. Agreement is a check on the agent's answer choice given the context it claims supports it. It is not a check that the bundle contains the right evidence or that all the relevant information was gathered. LangChain ran a similar pattern to score agent traces and found Jev cheaper and more repeatable than LLM-as-judge in their early test. They grade the investigator to monitor quality. Here the verdict gates admission to SMEme's reasoning pipeline; disagree, none fit, or low confidence, and the HITL sees both answers before anything becomes case evidence.

LLM agent ──▶ gathers evidence ──▶ state
    │                                │
    ▼                                ▼
proposes an option        Jev answers the same blind
    │                     question from state alone
    └────────▶ agree? ◀──────────────┘
         yes, confident  →  admission policy
         otherwise       →  a person sees both answers

The code

This is a sketch, not a packaged example. On September 21, 2026, I tested the Jev → LangGraph interrupt/resume → SMEme continuation path against Jev 1.13.0 and SMEme's hosted MCP surface. Jev chose an answer from SMEme's authorized options, a reviewer admitted it, and SMEme recomputed the theory and returned the next question. The gatherer, agent, and SQL adapters remain illustrative. The Jev calls follow TypeSafe's published Python SDK, and the SMEme calls follow our public MCP contract.

import hashlib, json
from typing import TypedDict
from langgraph.graph import StateGraph, START, END
from langgraph.types import interrupt, Command
from langgraph.checkpoint.memory import InMemorySaver
from typesafe_sdk import Choice, TypeSafeClient

jev = TypeSafeClient(model="jev-1.13.0")   # pin: thresholds are tuned per version
JEV_FLOOR = 0.5                            # first pass: escalate to an agent; after an agent: person if below
NONE_FIT = "__none__"                      # adapter-only escape; never sent to SMEme

# Deployment config, owned by the tree's operator — not by any model, and not by SMEme.
ROUTES = {                                  # SMEme question_id -> first node
    "q_us_incorporated": "jev",             # state already holds the evidence
    "q_ownership_disclosed": "gather",      # gather first, then Jev judges
    "q_beneficial_owner_verified": "agent", # agent investigates; Jev judges the bundle
    "q_sanctions_list_match": "sql",        # exact lookup proposes directly
}
AUTO_ADMIT = {"q_us_incorporated": 0.90}   # unlisted questions always go to a person


class Case(TypedDict, total=False):
    tree_id: str
    session_id: str
    subject: dict      # case state, assembled and filtered by retrieval/code
    task: dict         # SMEme blind task: question_id, stem, options
    proposal: dict     # option, confidence, source, provenance_id
    decision: dict     # what actually gets admitted (option may be None = abstain)
    report: dict       # SMEme's terminal report
    blocked: dict      # fail-closed pause (e.g. isolated_evaluations_required)


async def smeme(tool: str, **args) -> dict:
    # smeme_session: an authenticated MCP ClientSession for SMEme's MCP server
    result = await smeme_session.call_tool(tool, args)
    return json.loads(result.content[0].text)


def absorb(out: dict) -> dict:
    if out.get("report"):
        return {"report": out["report"], "task": None, "proposal": None}
    if out.get("task"):
        update = {"task": out["task"], "proposal": None, "decision": None}
        if "inquiry_session_id" in out:
            update["session_id"] = out["inquiry_session_id"]
        return update
    return {"blocked": out, "task": None}   # fail-closed; e.g. isolated_evaluations_required


def evidence_ref(subject: dict) -> str:
    # Fingerprint of the exact state that was judged. A production adapter should
    # point at the host's evidence bundle (document locators, record ids), so an
    # auditor can reopen what the judgment was *about*, not just who made it.
    return hashlib.sha256(json.dumps(subject, sort_keys=True).encode()).hexdigest()[:12]


async def start(case: Case):
    return absorb(await smeme("smeme_reasoning_evaluate",
                              decision_tree_id=case["tree_id"]))


def ask_jev(case: Case):
    # Jev judges only case["subject"]. Never put the agent's conclusion in
    # subject: TypeSafe notes Jev doesn't treat state as hostile.
    task = case["task"]
    keys = {f"opt_{i}": opt for i, opt in enumerate(task["options"])}
    criteria = {**keys, NONE_FIT: "None of the listed answers is supported by the state"}
    r = jev.system_one(
        state=case["subject"],
        questions={"q": Choice(instructions=task["stem"], criteria=criteria)},
    )
    a = r.answers["q"]
    judged = {
        "option": keys.get(a.choice),      # None when Jev picked NONE_FIT
        "confidence": a.confidence,
        "source": "jev",
        "provenance_id": f"evidence:{evidence_ref(case['subject'])}/jev:{r.model}",
    }
    prior = case.get("proposal") or {}
    if prior.get("source") != "agent":
        return {"proposal": judged}
    # Jev-as-judge: the agent already proposed; this checks the agent's choice.
    agree = judged["option"] is not None and judged["option"] == prior.get("option")
    if agree and judged["confidence"] >= JEV_FLOOR:
        return {"proposal": {**judged, "option": prior["option"], "source": "agent+jev"}}
    return {"proposal": {**judged, "source": "jev-judge",
                         "agent_option": prior.get("option")}}


async def ask_agent(case: Case):
    # Investigate and assemble evidence. Return a proposal separately so it
    # never lands in subject, which Jev will score next.
    # found holds source material (excerpts, records), not the agent's summary.
    found, proposal = await research_agent.investigate(case["task"], case["subject"])
    return {"subject": {**case["subject"], **found},
            "proposal": {**proposal, "source": "agent"}}


async def ask_sql(case: Case):
    return {"proposal": await lookup.propose(case["task"], case["subject"])}


async def gather(case: Case):
    # Assemble the evidence this question needs (a SQL query, a retrieve-and-filter
    # step, or an LLM agent reading across sources), then hand it to Jev. The new
    # state gets a new evidence fingerprint, so provenance tracks what was judged.
    found = await gatherer.collect(case["task"], case["subject"])
    return {"subject": {**case["subject"], **found}}


def admit(case: Case):
    p, qid = case["proposal"], case["task"]["question_id"]
    bar = AUTO_ADMIT.get(qid)
    judged_and_disagreed = p.get("source") == "jev-judge"
    if (not judged_and_disagreed
            and p["option"] is not None and bar is not None
            and p.get("confidence", 0) >= bar):
        return {"decision": {"option": p["option"],
                             "provenance_id": p["provenance_id"]}}
    # Otherwise a person commits: accept the proposal, change it, or abstain.
    # jev-judge carries agent_option so the reviewer sees both.
    return {"decision": interrupt({"question": case["task"], "proposal": p})}


async def commit(case: Case):
    d = case["decision"]
    args = {
        "inquiry_session_id": case["session_id"],
        "question_id": case["task"]["question_id"],
    }
    if d.get("option") is not None:
        args["selected_option"] = d["option"]
        args["provenance_id"] = d.get("provenance_id")
    return absorb(await smeme("smeme_reasoning_evaluate_continue", **args))


def next_step(case: Case):
    if case.get("report") or case.get("blocked"):
        return END
    return ROUTES.get(case["task"]["question_id"], "jev")


def after_jev(case: Case):
    p = case["proposal"]
    if p.get("source") != "jev":
        return "admit"   # already judged an agent's proposal
    return "agent" if p["option"] is None or p["confidence"] < JEV_FLOOR else "admit"


g = StateGraph(Case)
for name, fn in [("start", start), ("jev", ask_jev), ("agent", ask_agent),
                 ("sql", ask_sql), ("gather", gather), ("admit", admit),
                 ("commit", commit)]:
    g.add_node(name, fn)
g.add_edge(START, "start")
g.add_conditional_edges("start", next_step)
g.add_conditional_edges("commit", next_step)
g.add_conditional_edges("jev", after_jev)
g.add_edge("gather", "jev")
g.add_edge("agent", "jev")
g.add_edge("sql", "admit")
g.add_edge("admit", "commit")
graph = g.compile(checkpointer=InMemorySaver())

Run a case, and when the graph pauses for a person, resume it with their decision:

config = {"configurable": {"thread_id": "vendor-A-104"}}
out = await graph.ainvoke({"tree_id": TREE_ID, "subject": subject}, config)
# out["__interrupt__"] carries the question and the proposed answer
out = await graph.ainvoke(
    Command(resume={"option": "Yes", "provenance_id": "reviewer:jlee/kyc-file-3"}),
    config,
)
print(out["report"]["result_kind"])

Notice what isn't in this code. There are no branch conditions, no thresholds that combine answers into a conclusion, and nothing that encodes the approval policy. The routing table says who gathers evidence and who answers. Jev may answer first, or independently re-answer from an agent's bundle so the harness can check the agent's choice. The admission table says how much confidence a question needs before an answer is admitted without a person, and a disagreement between Jev and the agent always interrupts, following TypeSafe's Confidence-Gated Routing pattern. What follows from the answers lives in the deployed theory the expert authorized. The answerer component is shown the question and its options, but never the branching logic or possible conclusions.

Confidence meets commitment

Jev's most useful property here isn't speed. It's an explicit confidence signal the host can act on at the commitment boundary.

SMEme has two commitment boundaries. Rule commitment happened when the expert Deployed the tree, and nothing in this harness can touch it. Case commitment is admission, the moment a proposed answer becomes evidence in this matter. SMEme defines the proposition being admitted. The operator decides whether a Jev judgment is enough to admit it automatically. A low-stakes classification can auto-admit above 0.9. A question that decides whether we verified a beneficial owner always goes to a person, with the proposal pre-filled.

A person can also abstain, and the adapter has to be careful here. If the tree has a "Don't know" answer, choosing it is evidence the procedure can branch on. The adapter's none fit option is different. It isn't an answer at all. It becomes an abstention or an escalation, never a fact. Ordinary branching code has to represent that distinction explicitly and often collapses it into a default branch. SMEme gives it formal semantics. Unanswered means no commitment has been made, not false.

The guarantee is deliberately narrow. Given the procedure you authorized and the evidence you admitted, this is what follows. It doesn't certify that the evidence is true.

Speculative computation is fine. Speculative commitment isn't.

The sketch asks one question at a time because that is what SMEme Inquire returns. Jev's Speculative Fan-Out pattern does the opposite. It sends many narrow questions about the same state in one request and leaves it to code to decide which answers are relevant. Their smart-home demo demonstrates this pattern. "Turn off all of the lights in the house" goes out as one request carrying a catch-all list of questions about everything in the smart-home domain. Asking category, then device, then action, one call at a time, would be an anti-pattern for that use case. Code filters the answers afterward, or as the comment in their reference workflow triage_ticket.py example puts it, "Let code decide which speculative answers matter on this path."

That filter is where the two systems meet. For simple decisions, hand-written code is the right filter. For legal, medical, underwriting, or compliance decisions, deciding which answers matter is the decision procedure itself. That's where SMEme comes in. The expert writes the decision tree in plain language, reviews it, and authorizes it. When it's deployed, it's frozen. SMEme compiles it into a formal theory, and a symbolic solver reasons over the whole tree at once. The solver replaces that hand-written relevance filter with logical analysis of the expert's decision procedure. From the tree and the answers committed so far, SMEme logically infers which questions can still change the outcome and which cannot.

SMEme asks for one answer at a time, because the solver knows which question matters next. That doesn't mean Jev is called once per question. The harness can ask Jev everything the current evidence can answer in a single call and keep the results. When SMEme asks a question, the harness uses the answer it already has instead of calling Jev again. Some of Jev's answers will never be used, because the solver decides those questions are irrelevant given the admitted answer(s). They were cheap to compute, so nothing is lost.

The only thing that happens one step at a time is deciding which answers become part of the case. After each answer is committed, the solver works out what follows. Either a conclusion is reached, or it names the next question worth answering. Compute eagerly if it's cheap. Commit only the answers SMEme asks for, because those are the ones that can still make a logical difference.

Fan out within an evidence boundary

The natural unit of fan-out is an evidence-ready batch, meaning every Jev-routed question whose evidence is already in the state. That may or may not be the whole decision tree. Thirteen questions in one Jev call are thirteen parallel judgments, not thirteen steps of reasoning. SMEme treats the corresponding answers as jointly constrained. Admitting one answer can make another question irrelevant, while an unanswered one may still change the outcome.

There are two clocks in the harness. The evidence clock advances when subject changes. Jev can run wide over each evidence snapshot, and the fingerprint says which snapshot its answers belong to. The theory clock advances when an answer is admitted. SMEme recomputes what follows and Inquire returns the next unresolved question that can still matter. Cached Jev answers can satisfy that request without another model call, but they do not advance the theory clock by themselves.

The routes in the sketch create the evidence boundaries. q_us_incorporated can be included in an initial Jev batch because its evidence is already in subject. q_beneficial_owner_verified must wait until an agent assembles the beneficial-owner file. q_sanctions_list_match belongs to an exact lookup rather than a semantic judge. Once gathering changes the state, the old fingerprint misses and Jev can fan out again over the new bundle. This follows TypeSafe's own rule for a real second request, which is to make one when the later judgment cannot be constructed until new state exists.

The sketch leaves this batching out so the control loop stays visible. Fan-out changes how many ready judgments Jev computes at once. It does not change who decides what. Inquire decides which question can still matter, the harness gathers the evidence, Jev judges it, and admission decides whether the answer enters the case.

Apply is the natural batch path when a gathering procedure has already produced a complete, stable evidence bundle. Jev can fill the worksheet in one pass and SMEme can reason over the submitted answers together. Inquire is the demand-driven path when the file is incomplete or when acquiring the next answer may require an agent or a person.

That is the economic complement between the two systems. Jev runs wide over evidence you already have because those judgments are fast and cheap. SMEme keeps evidence acquisition narrow by asking only for unresolved facts that can still change the result. As in the oil-shock example, the expensive part is not judging another row. It is acquiring the evidence needed to answer it.

The model interprets the world. The expert defines the procedure. SMEme determines what follows.

Try it

SMEme Core is source-available under a Sustainable Use License, the same idea as n8n. You can self-host from GitHub. DeepWiki is the code map.

To install, use the hosted free tier at smeme.ai and the public MCP connector, or clone Core and follow the self-host quickstart. The appliance image is ghcr.io/AristaLabs/smeme. Either path gives you the same reasoning tools this sketch calls. If you have a decision you care about, I would like to run this harness with you on it.

Dan Arista, PhD
Founder & Managing Member
Arista Labs, LLC