PrismPath
Open SourceThe document your team reads is the graph the engine runs.
A control plane for autonomous systems. Define what a system is allowed to do in one Markdown document, prove that structure before it runs, enforce it where the system actually executes, change it without rebuilding the system, and get a signed receipt for every decision.
## Intake
Classify the incoming request.
-> Billing: about charges or refunds
-> Technical: about bugs or outages
-> General: else
## Billing
Pull the account and recent charges.
-> Resolved
## Technical
Check status; reproduce if you can.
-> Resolved
## General
Answer directly.
-> Resolved
## Resolved
Summarize what was done.The same file, two ways: what you read on the left is exactly what the engine runs on the right.
How it works
Prove what can happen. Enforce what may happen. Prove what happened.
A person writes the flow
Each heading is a step, each arrow an edge with a condition. Deterministic edges decide first and free, in document order; a model is reached only where meaning genuinely requires one. The predicates are authored, never compiled from prose.
Tooling proves it
Undefined targets, unreachable steps, unbounded cycles and always false edges are caught by validate; reachability under an assumption is model checked by verify; capability says which targets the flow compiles to.
The fragment compiles
Level M, the decidable fragment every substrate executes, becomes a table image of a few hundred bytes that carries a computed worst case bound.
The image is signed and swapped
A pack binds the image, its fields, its version and its bound to a key. A host checks the signature, the declared envelope and a monotonic version floor, flips atomically, and writes one audit event either way.
Every decision leaves a receipt
A one byte cause code says why the run routed, refused, parked or escalated. Receipts Merkle root per session and anchor to a timestamp a third party can verify without trusting the emitter.
What you get
- Policy as a Markdown document: readable, diffable, tested against a fixture table with no model in the loop
- Deterministic routing first, semantic routing where meaning needs it, a person when confidence is low
- Static analysis, reachability and bounded model checking before anything runs
- Signed policy packs with a declared envelope, a version floor and an atomic swap
- Receipts with cause codes, Merkle rooted trails, OpenTimestamps and RFC 3161 anchoring
- Four language kernels judged by one frozen corpus, plus in kernel, microcontroller and FPGA targets
PrismPath does not own the model, agent, orchestrator, operating system or hardware that produces a candidate action. A worker can be a hosted model, a local model, a shell process, a function or another orchestration system. PrismPath decides where the run goes next and records why.
## classify
Read the incoming support ticket.
Emit `category`, `amount`, and `sentiment`.
@emits(category, amount, sentiment)
-> human_review: when category == "billing_dispute" and amount > 500
-> billing: when category in ("billing", "billing_dispute")
-> outage: when category == "outage"
-> retention: when sentiment == "angry"
-> general: elseValidate it, test it against its fixture table, change one condition, watch the route change, read the receipt. That is the product; everything below it is why the promise can be kept.
Portability
Four kernels. One corpus.
Every kernel passes the same 1,079 predicate and 27 flow vectors, frozen in the repository. Author the policy once; run it in whatever language each service already speaks, and know they agree.
Python
P0 to P2The reference for the flow language. Full routing stack: embeddings, one shot model routing, lockfiles, checkpoints, the signed pack and the audit trail.
JavaScript
P0 to P1Zero dependency ES module. Browsers, Node, edge functions. The playground on this site runs it client side.
Rust
P0 to P1Native binaries, WASM, embedded. Compiles to every architecture Rust targets.
Go
P0Standard library only. Services and CLIs; a single static binary per platform.
Two tiers, kept distinct
P0, P1 and P2 say how much of a flow runs without a model. Level M is the decidable fragment inside P0 that the compiled images and every hardware target execute. The two are kept apart so nobody infers that a model backed route compiles to a chip.
Deterministic
No model. Every edge is decidable: when predicates, error edges, event edges. Runs on any kernel. Its Level M subset (field against constant, membership, truthiness, and, or, not) is what compiles to an image.
Locked semantic
Semantic edges pinned by a lockfile. Needs an embedder, but routing is reproducible.
Full engine
Live embedding plus one shot model routing, with abstention and human escalation. Python reference kernel required.
Before execution
Prove what a flow can, and cannot, do.
Because deterministic edges are decidable, PrismPath does not just run your routing; it can prove properties of it before it ever executes. prismpath verify runs bounded model checking over a flow and answers reachability questions with a witness path.
- “Can this node ever be reached?” Answered, with a concrete path that gets there.
- “Is the danger state unreachable once amount ≤ 500?” Assumptions are first class.
- Three valued honesty: yes, may, no. Never a false certainty.
- Routing you can audit and sign off, not just execute.
checking reachability (assume: amount <= 500) danger no unreachable (state space exhausted) resolve yes intake → triage → resolve PROVEN: 'danger' is unreachable once amount <= 500.
One authority model, many substrates
The same image, from a Python process to a chip.
The same signed image decided the same corpus readings identically on host Python, the C reference, in the Linux kernel on aarch64 and x86_64, on both instruction sets of an RP2350, and on a Zynq-7020 fabric. A Level M flow compiles to a table image that a fixed circuit interprets in fabric, or that a 1.7 KB interpreter runs on an 8 bit microcontroller. No OS, no runtime: the Markdown is the device’s program.
corpus vectors certified on the physical fabric, and in kernel on every push
cycles: the worst case witnessed on the fabric pins, inside the signed bound, across 16,009 evaluations
of a Zynq-7020 (1,064 LUTs), timing clean at 50 MHz
the whole AVR firmware, interpreter and serial protocol included
Microcontroller execution is certified across four instruction sets: 8 bit AVR, ARM Cortex-M33, RISC-V and Xtensa. The C, RTL and firmware interpreters are certified against the declared Level M subset of the frozen corpus; the subset is stated and never exceeded. Every number here is a row in the evidence ledger, hash anchored on Bitcoin.
Decision telemetry
Ship the decision, not the data.
A policy depends on only some distinctions in its input. Figueroa quantization derives, from the policy text, the cells of each field that can change a decision, and a reading is sent as one symbol per cell. Any representative of a cell routes identically. The Facet protocol carries those symbols, with the codebook agreed from the signed policy rather than sent.
- Decision preservation proven in Lean 4: thirteen theorems, zero sorry, on the standard axioms, within a declared domain of well typed integer readings.
- Stating the theorem found three defects in the reference quantizer, now fixed and pinned by the corpus.
- The Facet wire: self framing Fibonacci codes, per packet Merkle roots, a staleness bound by cadence, replay refusal with a named cause.
- About 1.5 B per decision with its integrity apparatus counted, 66.9 times under an OpenTelemetry record of the same decision, measured over 64,484 decisions.
- Decision lossless, not data lossless: raw magnitudes never leave the node.
Specified, proven, and measured in the open.
Figueroa quantization and the Facet protocol are the two named contributions: the decision sufficient map, and the wire that carries it. The wire is PrismPath’s own and composes with other engines; the comparison below carried OPA’s input on it.
Where it stands
One of many control planes. Compared in public.
A pre registered comparison against OPA, Cedar, Cerbos, OpenFGA and Openlane, frozen before any comparator was installed and run to the end on real systems and hardware, found that every property PrismPath builds in is reachable by at least one comparator with bounded glue. PrismPath is not a layer the existing engines cannot reach, and the verdict says so, because it is the credibility of everything else on this page.
The same table shows PrismPath native on all eight properties where no comparator is native on more than two; OPA reaches the row only with 391 lines of glue nobody ships; and on the same microcontroller the OPA path needs about 312 KB of RAM and a 136 KB module per policy against a 1.7 KB interpreter class and 224 B images. Differences of degree and composition, reported straight.
See it route in your browser.
The playground runs the JavaScript kernel client side: write a flow, watch it compile, share it as a link. Nothing you type leaves the page.