Neural proposes. Symbolic decides.

Horismos is an ontology-first decision kernel that sits between a policy and what it acts on — a planner and an actuator, an agent and its tools. Your rules make the call. A model can only propose typed facts. Every decision ships with a proof — and the kernel still runs with the model deleted.

Quickstart — 10 minutes, zero API keys Physical AI — the shield, with proofs Coming from LangGraph

No model required — the shield below runs on structured input alone Day one: an opt-in bridge for TypeSafe AI's Jev — typed answers, never prose Rust core · Python bindings Standard Turtle, RDFS-plus MIT OR Apache-2.0 Pre-alpha

Where the model is allowed to act Two declared boundaries. Nothing else calls a model.

The whole idea in a dozen lines

You have shipped a policy — a VLA model, an RL controller, an LLM planner — and it proposes each motion of an arm that works near people. Somewhere in a prompt or a reward it says "keep half a metre from a person, and slow down in a shared cell", and somewhere in production the model skipped that line. In Horismos the sentence is a rule in a small ontology file, the policy can only propose a typed command, and the rule — not the policy — decides whether it reaches the actuator:

Three commands, three proofs

from horismos import Ontology, World, HorismosValidationError
from horismos.examples import path

world = World(Ontology.load(path("gallery/safety-envelope.ttl")))

def shield(subject: str, **state: object) -> None:
    cmd = world.assert_(":MotionCommand", subject=subject, **state)
    print(world.explain(cmd, ":verdict").render())

shield(":cmd-1", zone=":OpenFloor", nearest_human_distance=2.4,
       requested_speed=1.8, e_stop_engaged=False)
shield(":cmd-2", zone=":SharedCell", nearest_human_distance=0.8,
       requested_speed=1.2, e_stop_engaged=False)
shield(":cmd-3", zone=":SharedCell", requested_speed=0.4, e_stop_engaged=False)

:verdict = :Permitted   via permitOpenFloor — "Open floor with clear separation — command permitted as proposed"
  ├─ eStopEngaged false is false   (asserted by the api)
  ├─ zone :OpenFloor is :OpenFloor   (asserted by the api)
  └─ nearestHumanDistance 2.4 atLeast 1.0   (asserted by the api)

:verdict = :Attenuated   via attenuateInSharedCell — "Shared cell with a person present — speed is capped, command is attenuated"
  ├─ eStopEngaged false is false   (asserted by the api)
  ├─ zone :SharedCell is :SharedCell   (asserted by the api)
  ├─ requestedSpeed 1.2 exceeds 0.25   (asserted by the api)
  └─ nearestHumanDistance 0.8 atLeast 0.5   (asserted by the api)

:verdict = :Blocked   via noProximityReadingBlocks — "No proximity reading — the minimum separation distance cannot be established, so motion is refused"
  ├─ eStopEngaged false is false   (asserted by the api)
  ├─ zone isNot :Restricted   (closed world)
  └─ nearestHumanDistance isEmpty   (closed world)

The third command is the one to look at. No distance reading arrived, and the shield did not read silence as safety: it refused, with a proof whose leaf names the reading that never came. Now try to set the verdict directly — the way a policy network, a tool, or a careless caller would:

Refused — every path into the world, no back door

try:
    world.assert_(":MotionCommand", subject=":cmd-4", zone=":OpenFloor",
                  requested_speed=0.1, e_stop_engaged=False, verdict=":Permitted")
except HorismosValidationError as e:
    print(e)

verdict may only be assigned by rules (horis:assignedBy horis:RulesOnly); assertion came from the api

That refusal is the product. It applies to every path into the world — perception, rule, tool, API — with no back door, and nothing above needed a model or a key. The snippets run verbatim against the installed package. Physical AI takes the same overlay through the mechanical limit, the emergency stop and the two coverage gaps verify() found; the quickstart walks through the kernel with nothing to configure.

The same kernel, a clinical overlay

The flagship example is clinical triage, and it shows a step the shield never needs. No rule here mentions crushing chest pain; the imported SNOMED subset says it is a kind of chest pain, and the proof shows that step:

The proof, not a transcript

from horismos import Ontology, World
from horismos.examples import path

onto = Ontology.load(path("triage/triage.ttl"),
                     imports=[path("triage/snomed-ct-subset.ttl")])
world = World(onto)

p = world.assert_(":Patient", subject=":p7",
                  heart_rate=128, has_symptom=[":CrushingChestPain"])

print(world.explain(p, ":acuity").render())   # derived by rule r1 inside the same transaction

:acuity = :Immediate   via r1 — "Tachycardia with chest pain — immediate track"
  ├─ heartRate 128 exceeds 120   (asserted by the api)
  └─ hasSymptom :CrushingChestPain ⊑ :ChestPain   (subsumption)

Rules written against concepts grow their coverage with the vocabulary rather than with the prompt. The Health page and the quickstart carry the full clinical walkthrough, including the same RulesOnly refusal for acuity.

What breaks in prompt-governed agents

These are the failure classes working agent teams keep meeting, and a robot makes every one of them physical: a silent wrong state is a wrong motion, and an approval that was correct at check time can be stale by actuation. Every number below is measured in the primary source cited beside it, not by us.

Silent wrong-state failures — the run "succeeds", the state is wrong, no tool errored

What was measuredIn τ²-bench airline, 78% of observed failures were silent wrong-state failures with no tool error; deterministic read-only pre-execution gates raised task success from 29.6% to 42.0% (arXiv:2607.07405)

What Horismos does insteadEvery write passes a five-check gate in domain terms; rule-derived facts are recomputed, never left stale (The World)

Stale approvals — correct when checked, stale when acted on

What was measuredApproval verdicts changed in 5.3–48.4% of cases after an eight-step replay shift (arXiv:2608.26306); models produced stale-aligned decisions 74.7–77.3% of the time, while version-stamp checks were 100% deterministic (arXiv:2608.25553, arXiv:2609.00243)

What Horismos does insteadDecisions are scoped to a versioned snapshot; a commit against drifted source state fails closed (Guarantees)

Prompt injection flipping the conclusion

What was measuredUnder injection, five open models inverted a verified conclusion in 61% of trials; a hardened prompt cut that to 14%; only enforcement drove it to zero (arXiv:2606.19588). Six LLMs repeated a single planted fake lab value in 50–83% of clinical vignettes (Communications Medicine, 2025)

What Horismos does insteadPerception can only propose schema-forced facts; decision properties are unrepresentable in its output; narration renders only from the proof (LLM Boundaries)

Policies that cannot see state

What was measuredCodex rules "evaluate command prefixes only — they cannot reference repository state"; after PocketOS lost production data to a blanket-scope token, the post-mortem read "guardrails must be implemented at the API gateway and token-permission level, not in advisory text" (Codex rules documentation; AIID 7311)

What Horismos does insteadPreconditions are declared over typed world state and checked by the runtime before any tool fires (Tools)

What you get

• A typed world, not a scratchpad. Facts are instances of ontology classes; ranges, units, cardinality, closed enumerations and provenance policy are enforced at the gate. Rejections are sentences an auditor can read: requestedSpeed 3.5 exceeds horis:max 2.0 (m/s) on :MotionCommand.
• Rules that decide, with proofs. Deterministic forward and backward chaining, subsumption over your class hierarchy and imported vocabularies, a proof tree per conclusion, and truth maintenance that re-derives when base facts change.
• LLMs at two declared boundaries only — and optional. Perception (text → typed instances, schema-forced, confidence-gated, with a mandatory fallback edge) and narration (proof → prose, never written back). Structured input — a sensor reading, a planner's command, a record — skips the model entirely, which is why the shield above needs none.
• Tools the runtime fires. Declared contracts: typed arguments read from the graph, preconditions checked, effects validated through the same gate. The model never picks a tool or builds its arguments, and a policy never marks its own command safe.
• Traces as the product. Every run emits a typed, replayable trajectory — the audit log and the training corpus are the same object, with loss masks precomputed.
• Verification before deployment. Completeness, conflict-freedom, dead rules, termination and workflow totality, with counterexamples rendered in domain terms. Ontology.load refuses an ontology that fails them (see Guarantees for exactly what is claimed).

When the model is the boundary

Everything above is a discipline the kernel imposes on a model that would happily do more. TypeSafe AI's Jev is the other case. It is a text → decisions model: it takes free text plus a set of typed questions and returns one typed answer each — a probability, an option key, or an ordinal level. It has no text output channel at all. Not instructed not to write prose. Cannot.

Routed through the perception boundary, Jev proposes and only proposes. JevBridge translates the perception schema the runtime derives from your ontology into those three primitives: a boolean property becomes a probability, a closed vocabulary becomes a choice, an enumeration a deployment declares ordinal becomes a score. An ontology names it the same way it names any other model — horis:model "jev:jev-1.13" — and routing is per step, so a workflow can send perception to Jev and narration to a text-capable bridge in the same run. Ask Jev itself to narrate and it refuses without making a call: the model has no text output channel, and the bridge will not stitch prose out of answer keys.

Ask it for something it cannot answer — a number, an open string, a date-time — and it refuses there too. It does not bucket the number into a score and it does not quietly drop the property. The call fails, naming the property, and the step takes its horis:fallback edge like any other bridge error, because approximating it as a score would fabricate a measurement under perception provenance. A heart rate belongs on the structured-input path, with the real reading and the real source. The refusal is the design, not a gap.

Here is a whole decision. One line of a ward note, four typed booleans with a probability each, and the three rules in examples/vte/vte.ttl reaching a recommendation that carries horis:assignedBy horis:RulesOnly — so it is absent from the schema the model is shown. The model has no way to express the decision. Not discouraged: absent.

Typed answers in, a derivation out

make demo-jev — second note, token and cost lines trimmed

78yo, post-op day 2, on warfarin, bed-bound

Jev proposed these typed facts, one parallel pass:
  reducedMobility    true   p=0.940  ███████████████████████·
  activeCancer       false  p=0.910  ██████████████████████··
  priorVte           false  p=0.720  █████████████████·······
  bleedingRisk       true   p=0.610  ███████████████·········

call confidence 0.610 (the weakest fact in the call — nothing averages away)
instance[0] confidence 0.610

The rules decided. The model had no vote:
  :recommendation = :HoldProphylaxis   via bleeding-contraindication — "Bleeding contraindication — hold pharmacologic prophylaxis"
    └─ bleedingRisk true is true   (asserted by perception)

On warfarin is the ambiguity — already anticoagulated reads as a reason to hold pharmacologic prophylaxis, but the note never says so outright — and the answer set says so, at p=0.610. That transcript is the mock's: its probabilities are authored stand-ins, not a model's measurements. Both the per-instance and the call-level confidence are the weakest answer they cover, never an average, so one coin-flip cannot hide behind three certainties when the runtime compares against horis:confidence. Every proposed fact still clears the same five-check gate on the way in; perception provenance buys no exemption.

make demo-jev prints that transcript deterministically against the mock — no key, no network. make demo-jev-live builds in the real client; bridges-jev is default-off, like every bridge that carries TLS. Either way it is the same Bridge trait an ordinary chat model implements, and the kernel takes both unchanged. The full treatment — the schema-shape-to-primitive table, why a jev: step extracts exactly one class, and what the bridge deliberately refuses to guess — is in The Bridge.

It surrounds your stack

Horismos does not replace your planner or your controller, LangGraph, your agent SDK, your coding harness, or your system of record — and it does not replace the safety-rated stops a cell already has. It gates one decision inside them.

See Architecture for the bounded projection kernel in one diagram, and Coming from LangGraph for the honest split of who does what.

What Horismos does not claim

Stating the edges plainly is part of the offer.

• It does not verify the LLM. Verification proves the symbolic system is total and sound around whatever perception does; the mitigation for a bad extraction is the gate, the confidence threshold and the fallback edge — not a promise about the model.
• It does not prove generated code is correct. For coding agents, the planned candidate-artifact boundary proves a proposal was policy-legal and passed its declared checks. Semantic correctness stays a review and test claim.
• Its guarantees are snapshot-scoped. Inside one evaluated projection the gate has no back door and determinism holds. Freshness and completeness are only as good as the last hydration and the declared input closure.
• It is not a system of record, an orchestrator, or OWL-DL. It overlays your records, runs one bounded decision, and takes RDFS plus a small executable vocabulary — full description-logic inference is out of scope forever.
• It is not a safety-rated component. Horismos is a supervisory decision layer between a planner and an actuator interface, not a safety PLC or a control loop; it makes no claim against ISO 10218, ISO/TS 15066 or IEC 61508 and has not been assessed under them.
• It is pre-alpha. Every published release so far is a pre-release (pip install horismos installs the latest; see the Quickstart), and the surface can still change between them.

Where next

• Physical AI — the shield end to end: the mechanical-limit refusal, the emergency stop recomputed in the transaction that recorded it, and the two coverage gaps verify() found and what closing them took.
• Quickstart — make develop, load an ontology, watch the gate reject bad data, print a proof, run the full agent loop on the mock bridge, then go live with one environment variable.
• Go live in 2 minutes — the same demo against a real model through OpenRouter: one environment variable, a real captured trace, and a decision and proof identical to the mock run.
• Coming from LangGraph — the same decision written both ways, and the ten lines that let a graph node call the kernel.
• Governing a coding agent — a 28-term change gate where the bot cannot grant itself merge permission.
• Use cases — health, coding, insurance, physical AI, customer operations: one template, five runnable overlays.
• The guarantees, honestly — what verify() proves, what is explicitly not claimed.
• Framework reference — the shipped-voice definition, docs 00–15.