Introduction

This site is the code-derived documentation for Nibli: a zero-hallucination symbolic reasoning engine with a human-readable knowledge-representation surface (nibli KR).

These pages track main, not a released tag — they are rebuilt on every push that touches mdbook/. The badges above show the latest release and the current published crate version; where the two could differ, the repository is authoritative. Released API docs are versioned on docs.rs.

It is not the Orange AVA book manuscript. Book rights are reserved by the publisher. Nothing here is copied from that manuscript. Claims should re-derive from the repository: source code, tests, just recipes, shipped corpora (.nibli files), and the root engine specifications.

Where to run things

Primary host path is /docs/nibli/; the GitHub Pages project site uses base path /nibli/. CI builds the mirror with site-url=/nibli/. Prefer relative links inside chapters so both bases work.

Open the playground →

Source layout

Open work — engine, tooling and docs alike — is tracked in TODO.md at the repository root.

Start here

1. What Nibli guarantees — the four-valued contract and scope.
2. Quickstart — Nix + just run.
3. nibli KR cookbook — surface syntax cheat sheet.
4. Playground — browser triad without installing anything.
5. Authorization — builtin policy and multi-language can / field masks.

User guide — overview

Audience: people writing .nibli knowledge bases, using the REPL or playground, or embedding the engine.

Deeper sources (repo root)

Query model: state a claim to check for entailment (e.g. dog(Adam).), not an interrogative. The playground’s decorative ? is not sent to the engine.

The developer guide covers the crate map, the IR, the WASM/host/compute path, the CI gates, and the WIT surface; published crate APIs are in the API index. Remaining docs work is tracked in TODO.md.

What Nibli guarantees

Derived from the engine README and GUARANTEES.md. The full contract text lives in those files; this page is a short operator summary.

One surface language

Nibli has one front-end language: nibli KR (predicate-call surface: dog(Adam)., animal(every dog).). Name resolution is fail-closed: an unknown word is a compile error, never an arity-guessed new predicate. Normative spec: NIBLI_KR.md.

Soundness (relative to what you asserted)

The engine never returns TRUE for a formula that does not follow from the asserted facts and compiled rules plus any proof-local compute checks evaluated for that query, given a correct implementation and correct trusted backend replies. A TRUE answer comes with a formal proof trace. Bugs would be deterministic and testable — not stochastic fabrication.

This is not omniscience: change the premises and the verdict can change.

Proof sources are explicit. A stored tuple is not automatically called a user assertion: Asserted names every active fact id and label, Derived cites the rule assertion and grounded premises even for eagerly forward-chained facts, and legacy existential-import evidence is Presupposed. Duplicate assertions remain separately citable; retraction and reopen reconstruct citations from the same authoritative assertion registry. Equality substitution cites the real stored equality path it used.

Ordinary-predicate temporal rule literals are flavor-exact. Bare rules are unqualified and do not silently lift into past, now, or future; authors declare same- or cross-flavor mappings explicitly. Negation-as-failure follows the same rule: bare ~P checks bare P, while past ~P checks only for a Past witness. Stratification remains conservatively keyed by surface relation, so temporal flavors cannot be used to evade a negative-cycle rejection. Identity and query-time compute built-ins retain their separately documented semantics. One formula path may carry one temporal prefix or one deontic prefix, never both. must past P and past must P are compile errors rather than formulas whose outer wrapper could be lost in the one-flavor fact/rule store. The same fail-closed rule applies to manually nested raw IR before assertion or query. It is path-scoped, so separate rule literals may use different flavors, as in an explicitly declared past P -> must Q mapping.

Closed world and closed domain

Inference assumes:

• Closed world — a fact you did not assert is taken to be false, not unknown.
• Closed domain — quantifiers range only over entities the knowledge base knows.

The default clean-core profile does not infer existence from a universal: animal(every dog). alone makes no dog, and some dog remains plain ∃. Legacy xorlo import is an explicit opt-in (NIBLI_EXISTENTIAL_IMPORT=1 or :existential-import on). When enabled, the imported witness is a full logical entity: it participates consistently in ∃/∀/find/count/aggregate. Find and proof metadata label it existential-import, count proofs disclose the imported share, and the host/UI show which profile is active. Toggling the profile rebuilds the current KB transactionally, so existing rules change immediately.

Ordinary reasoner-minted witnesses are labeled generated-witness; asserted user constants remain knowledge-base, even when their display text resembles sk_N. Internally, generated witnesses have source-scoped typed identities (source assertion, binder ordinal, sort, and origin). Their friendly sk_N or sk_N(argument) rendering is never semantic, so equal-looking user constants stay distinct through equality, event joins, find/count, proof, persistence, retraction, and rebuild. A compute call that would expose an internal witness to the string-only backend protocol fails closed as UNKNOWN (backend-unavailable); an equal-looking user constant still dispatches normally.

Exact counts are observations, not constraints

exactly N and no are query-only formulas over the current closed domain. They count identity-equivalence classes and disclose any legacy existential-import contribution in the proof. Assertion ingress rejects them before allocating a fact id: Nibli does not persist or enforce cardinality constraints, and exactly 0 is never a stored prohibition. Assert ordinary facts, then re-query after additions, equality changes, or retractions. Counts inside opaque fact { … } or event { … } content remain quoted content and do not constrain the outer KB.

Four-valued outcomes

How to read a query result (product README wording):

All four are QueryResult variants in the engine itself, not host conventions — RESOURCE_EXCEEDED carries which limit was hit. Raise them with the NIBLI_FUEL / NIBLI_MEMORY_MB env vars or the :fuel / :memory REPL commands; see GUARANTEES.md.

Witness enumeration has a separate complete-or-error contract. Native query_find/count_witnesses, and WIT query-find-text, return a reasoning error if any evaluated candidate leaf is UNKNOWN or RESOURCE_EXCEEDED; they do not turn an undecided membership into an empty row set or partial count. This includes non-finite arithmetic and negated non-definitive leaves, even if another OR branch is true. Definitive TRUE/FALSE enumeration is unchanged. Native aggregate inherits the same refusal before numeric projection, and the projection itself fails closed: a binding set that does not bind the variable, a non-numeric value, a non-finite operand, and a non-finite (overflowed) result each refuse with a distinct error instead of silently dropping rows. A complete empty enumeration is the typed AggregateOutcome::Empty; a valid aggregate carries its contributing-witness count as provenance (AggregateOutcome::Value { value, witnesses }). Exact-count formulas use their separate domain-based CountNode evaluator and are not changed by this collection rule, including the disclosed NaN-only domain boundary.

Trusted proof-local compute

Results from the external compute backend (exponential, logarithm, or another registered corpus relation) are trusted evidence for the current ComputeCheck, not stored premises. Registration is post-compile routing: it accepts an existing corpus spelling or canonical relation, normalizes aliases/committed compounds to the canonical IR name, and declares neither vocabulary nor arity. An unknown registration is refused and remains a text compile error. Native raw-IR callers may instead query an arbitrary explicit ComputeNode without registration; that remains query-only. The shipping component has no raw-buffer query or vocabulary/schema method, so a custom host backend cannot add an arbitrary text predicate by itself.

Built-in arithmetic (product / sum / quotient) follows the same proof-local lifecycle: no compute result enters the fact store or registry, receives an id, changes the domain, survives replay, or triggers forward chaining. Compute atoms are query-only; assertions and rules containing executable compute are rejected before an id is allocated, while quoted abstraction content remains opaque. The reference names exponential/logarithm are query-only as assertions even before registration, and registering a corpus relation while live stored facts or rules reference its canonical name is refused with the blocking ids named — registration order cannot strand a stored fact. The numeric comparisons (greater / less / num_equal) are query-only on the same terms whenever an operand could be a number: they decide a verdict and filter witnesses, but a rule may not carry one, so there is no numeric threshold rule. That is a decision rather than a gap — a comparison in a rule would be looked up in a store that never holds one, which is inert as a positive guard and, under ~, succeeds for every binding. A comparison between two named things (greater(Alis, Bob), “taller than”) is an ordinary relational fact and asserts normally. Each top-level query recomputes or redispatches; repeated identical external checks may share a transient within-query memo only to keep the verdict and proof consistent. A backend error is always UNKNOWN (backend-unavailable), even after an earlier successful query or when an ordinary fact has the same tuple. Any conclusion that uses a successful external check is only as sound as that oracle.

The stock external-compute path is deliberately low-assurance: plaintext, unauthenticated JSON Lines over TCP, with no identity, integrity, request binding, version, freshness/replay, revocation, or audit receipt. Any parseable Boolean received in stream order is trusted, so a valid forged, replayed, stale, or mismatched reply is not detectable. Stronger admission belongs in a custom native dispatcher, custom component host, or external secured transport; the stock :backend setting only selects an address. See WASM, host & compute.

Where the full story lives

• GUARANTEES.md — differential oracles (Vampire / clingo), Lean proofs, determinism, mutation baseline.
• LOGIC_IR.md — the FOL intermediate form the reasoner consumes.
• CI: just ci, just verify-soundness, just verify-proofs.

Quickstart

Source: README — Getting Started and the root Justfile.

Prerequisites

• Nix — rustc, cargo-component, just, wasmtime, mdbook, and the rest come from flake.nix.

Enter the shell and run the REPL

# From the nibli repository root
nix --extra-experimental-features 'nix-command flakes' develop

# Build the pipeline component + native host and launch the REPL
just run

just run is the full local operator path (WASM component + nibli-host). For a fast native check only:

just test          # unit tests (lib)
just check         # type-check workspace

First claims

In the REPL, assert facts and rules, then query by stating a claim (not asking a question):

animal(every dog).
dog(Adam).

Then query:

animal(Adam).

Expect TRUE with a proof when the rule and fact support the claim. See What Nibli guarantees for how to read FALSE vs UNKNOWN.

A larger starter table lives in the nibli KR cookbook. The repo root also ships example files such as readme.nibli, gdpr.nibli, and drug-interactions.nibli (:load path in the host REPL) — worked tours in the GDPR walkthrough and the drug-interactions walkthrough.

Dictionary note

The vocabulary is committed Rust source (nibli-lexicon/src/corpus/) — no network fetch at build or runtime. Local, CI, and the hosted playground share the same corpus.

Docs site (this book)

just docs          # build → mdbook/book/
just docs-serve    # http://127.0.0.1:3000

Prefer not to install?

Use the hosted playground — the engine runs fully in the browser.

nibli KR cookbook

Short surface cheat sheet. Normative reference: NIBLI_KR.md (v0.1). Executable grammar: nibli-kr/src/nibli_kr.pest. Examples match the product README language table.

nibli KR is a strict predicate-call surface: one statement per line, ending with a period. Unknown predicate words are a compile error, never a guess — names resolve through the committed English corpus, fail-closed.

Common patterns

exactly N and no compile as count formulas only for querying. They cannot be asserted as persistent cardinality constraints; assert ordinary facts and re-query the current count.

Predicates and places

dog(Adam).
goes(Adam, destination: some market).

• Positional args fill places in order; named args use corpus place labels (destination:, …).
• Converted aliases and compounds are dictionary-driven; uncurated a+b compounds fail closed.

Rules

animal(every dog).
eats(every animal).
dog(Adam).

Description-style universals (every dog) compile to rules. Explicit prenex:

all $x: dog($x) -> animal($x).

For ordinary predicates, temporal wrappers are part of each rule literal’s meaning. A bare rule is unqualified; it is not automatically projected into the past, present, or future. Declare same-flavor taxonomy or cross-flavor causation explicitly:

all $x: past dog($x) -> past animal($x).
all $x: past eats($x) -> now be_hungry($x).

With only all $x: dog($x) -> animal($x)., a past dog(Adam). fact does not derive past animal(Adam).

Choose exactly one prefix family per atom. past ~eats(Adam). and must ~eats(Adam). are valid, while must past eats(Adam). and past must eats(Adam). are compile errors. This restriction is per formula path, so separate rule literals may still declare a mapping such as past P -> must Q.

Negation-as-failure

~eats(Adam).

Stratified NAF under closed-world assumptions — see GUARANTEES for oracle coverage. Unstratifiable programs are rejected at assert time.

Where to go next

• Full construct inventory and profiles: NIBLI_KR.md
• IR after compile: LOGIC_IR.md
• Try it without installing: Playground

Playground

The Transparency Triad UI runs the full pipeline (nibli-kr → nibli-semantics → nibli-reason) in the browser. There is no nibli server.

Open playground →

Local equivalent: just ui (Dioxus on port 8080). Ship path: DEPLOY.md.

Panes

The nibli KR pane is the knowledge base. Each query rebuilds a fresh engine, re-asserts the KB, then runs the claim.

Query model

State a claim, do not ask a question:

eats(Adam).

The UI may show a decorative ? next to the query box — it is not part of the text sent to the engine. Verdicts are TRUE / FALSE / UNKNOWN (see guarantees).

Exact-count forms (exactly N and no) belong here in the query box, not in the KR knowledge-base pane. They report the current KB snapshot; the engine has no persistent cardinality-constraint assertion.

Formalize (optional)

Formalize (not “compile”) is a bring-your-own-key LLM step from the Source tab. The key stays in tab memory only; the request goes from your browser to the provider you choose. Drafts are checked by the real nibli-kr + nibli-semantics + render round-trip gates, plus a KB-assertability guard that rejects query-only exact counts, before they land in the KR pane. Formalize sits outside the deterministic reasoning core — always review the KR and back-translation.

Example knowledge bases (preset hooks)

The header dropdown loads preloaded KBs used in regression tests and demos. Treat them as example corpora, not as chapters of any third-party book. In example mode the KR is read-only and Formalize is disabled; the query control becomes a preset list that auto-runs.

The dropdown names and preset labels below are byte-stable hooks — they are defined in nibli-ui/src/examples.rs, pinned by the shipped_examples_compile guard (just test-ui), and safe to reference from docs and links:

The GDPR, utopia, and drug KBs are include_str!-ed from the same repo-root .nibli files the engine’s regression tests pin, so the playground cannot drift from the tested corpora.

Belief revision: edit and re-query

Each query rebuilds a fresh engine from the KR pane, so revising the KB is just editing it: delete or #-comment a fact line and re-run the claim. Presets are read-only — to revise one, paste its corpus into Custom mode first. Worked demos: Belief revision.

Built-in vs external compute

In-browser: built-in arithmetic (product / sum / quotient) and numeric comparisons work locally. External compute backend predicates need the host + backend path (just run-with-backend) — not the pure playground.

Both are query-only. A comparison decides a verdict and filters witnesses, so a threshold reads as a query; it cannot be a rule guard, and asserting one is a compile error. See Guarantees.

More

• Quickstart for the CLI REPL
• nibli KR cookbook for syntax
• Product UI notes in the README

GDPR walkthrough

A worked compliance knowledge base: a formalizable slice of the EU General Data Protection Regulation (Articles 5, 6, 7, 9, 15, 17, 33), answered by deterministic, auditable deduction.

Source of truth: gdpr.nibli at the repo root. Every verdict quoted below is pinned by the gdpr_* regression tests in nibli-engine/tests/integration.rs, so this page cannot silently drift from the engine. The same corpus ships as the playground preset “GDPR compliance (Ch 19)” — an example KB, not a chapter of any third-party book.

The scenario

Second-order legal concepts are mapped onto proxy predicates, disclosed in the corpus header:

Load it in the REPL

:load gdpr.nibli
[Load] Done: 24 asserted, 77 skipped, 0 errors

The 77 skipped lines are comments and blanks. Fact ids are assigned in file order; the consent fact approves(Adam). lands as fact #21 — the corpus deliberately defines the Article 17 rule after the scenario so these ids stay stable (a rule’s position in the file never affects reasoning).

Engine-checked queries

Query by stating a claim with the ? prefix. All verdicts below are asserted by the regression suite against the full loaded corpus:

Every FALSE here is a deduced false under the closed-world assumption — the engine exhausted the search — not a shrug. ? also prints a plain-English [Why] summary and the proof tree; see What Nibli guarantees for the verdict contract.

Belief revision: withdrawing consent

The headline demo. Adam’s only lawful basis is consent (fact #21). Retract it and re-query — both verdicts flip:

:retract 21
[Retract] Fact #21 retracted. KB rebuilt.

? permitted(Adam).
[Query] FALSE

? ~permitted(Adam).
[Query] TRUE

No lawful basis remains, so the right to erasure (Art 17(1)(b)) arises. The erasure verdict is derived by negation-as-failure and its proof carries the naf_dependent flag — the engine discloses that the conclusion rests on an absence. Nothing was edited by hand: the same rules, re-derived over the surviving facts. See Belief revision for the mechanics.

The corpus also stores Article 17 as a rule with a negated restrictor:

obliged(every person where ~approves, event { removes() }).

where ~approves compiles to a negation-as-failure check per subject: a consenting person carries no erasure obligation while a non-consenting one does (pinned by gdpr_erasure_rule_is_per_subject and the rule-level belief-revision test).

Honest boundaries

Two scope decisions the corpus makes explicitly, in its own comments:

• Art 7 (“freely given” consent) is deliberately not encoded. Whether a consent was un-coerced is a case-by-case human judgment — it stays outside the deductive firewall rather than being faked as a rule.
• The erasure rule keys on ~approves, not ~permitted. The corpus derives a lawful basis from a legal obligation, so a where ~permitted rule would close a negative basis↔obligation cycle — the engine correctly rejects that as unstratifiable at assert time. For Adam, whose only basis is consent, the two formulations coincide, which is why the right can equivalently be queried as ~permitted(Adam).

Try it in the playground

Select “GDPR compliance (Ch 19)” in the playground header dropdown. Its preset queries are exactly the first four claims above: lawful basis? (Art 6) · right to erasure? (Art 17) · a controller is not a consenting person—exhaustive FALSE · health record → personal data (Art 4/9, derived). Proofs render with the curated legal-domain overlay (“has a lawful basis for processing”), never a bare variable.

Drug-interactions walkthrough

A worked safety knowledge base: pharmacokinetic drug-drug interaction (DDI) reasoning — “should this co-prescription raise a safety alert?” — decided by deduction over an explicit mechanism instead of a statistical guess.

Source of truth: drug-interactions.nibli at the repo root. Every verdict quoted below is pinned by the ddi_* regression tests in nibli-engine/tests/integration.rs. The same corpus ships as the playground preset “Drug interactions (Ch 20)” — an example KB, not a chapter of any third-party book.

The scenario

The warfarin + fluconazole interaction, mediated by the CYP2C9 enzyme: fluconazole inhibits CYP2C9; warfarin (narrow therapeutic index) is metabolised by CYP2C9, so its concentration rises → toxicity risk → safety alert. Apixaban is the negative control: metabolised by CYP3A4, which fluconazole does not inhibit → no alert, as a real deduced FALSE. Phenytoin is the second control: pharmacologically at risk, but not on the patient’s chart.

The corpus has no native pharmacology vocabulary, so it maps onto the nearest committed relations and discloses the mapping in its header:

Enzymes are opaque rigid Names: Siptucin = CYP2C9, Sipcivon = CYP3A4.

The three-step mechanism

Step 1 — concentration rise. Grounded conditionals per affected substrate (the fully general join rule all $a, $b, $e: prevents($a,$e) & metabolized_by($b,$e) -> increases($b). also compiles and reasons correctly — the grounded form is an encoding choice, not a limitation):

prevents(Flukonazol, Siptucin) & metabolized_by(Varfarin, Siptucin) -> increases(Varfarin).

Step 2 — toxicity risk. One general rule with a conjunctive restrictor; both conditions are required:

dangerous(every chemical where increases where thin).

A wide-margin drug whose concentration rises is not flagged, and a narrow-index drug with no interaction is not flagged (both negative controls are pinned by ddi_toxicity_requires_both_conditions).

Step 3 — the alert is patient-gated. Risk is drug-level pharmacology; the actionable alert only fires for an at-risk drug this patient actually takes:

all $da: dangerous($da) & uses(Adam, $da) -> warns($da).

Load it in the REPL

:load drug-interactions.nibli
[Load] Done: 16 asserted, 78 skipped, 0 errors

Two fact ids matter for the belief-revision demos below (assigned in file order, pinned by ddi_corpus_transcript_pins): the inhibition fact prevents(Flukonazol, Siptucin). is #4, and the regimen fact uses(Adam, Varfarin). is #10.

Engine-checked queries

The phenytoin pair is the point of step 3: pharmacological risk is general, the actionable alert is patient-specific.

Witness extraction (??) enumerates bindings instead of checking one claim — “which drugs are CYP2C9 substrates?”:

?? metabolized_by($da, Siptucin).

lists warfarin and phenytoin as witnesses for $da; apixaban (a CYP3A4 substrate) does not appear (pinned by ddi_witness_cyp2c9_substrates).

Belief revision: two clinical moves

Alerts are never baked in — they are re-derived from current facts, so the two canonical chart edits are single retractions (see Belief revision):

Discontinue the inhibitor (retract prevents(Flukonazol, Siptucin)., #4): the mechanism’s entry premise disappears, so the concentration rise, the toxicity risk, and the alert all dissolve in one step — for both substrates, since they share the inhibitor:

:retract 4
[Retract] Fact #4 retracted. KB rebuilt.

? warns(Varfarin).
[Query] FALSE

? dangerous(Fenitoin).
[Query] FALSE

Discontinue the drug (retract uses(Adam, Varfarin)., #10): the alert is withdrawn while the drug-level risk stays derivable — the alert is gated on the regimen, the risk is not:

:retract 10
[Retract] Fact #10 retracted. KB rebuilt.

? dangerous(Varfarin).
[Query] TRUE

? warns(Varfarin).
[Query] FALSE

Both moves are pinned by ddi_belief_revision_discontinue_inhibitor and ddi_belief_revision_discontinue_drug.

Try it in the playground

Select “Drug interactions (Ch 20)” in the playground header dropdown. Its presets are the headline chain plus the negative control: concentration rising? · toxicity risk? · safety alert?—a 3-hop proof · negative control—no alert. Proofs render with the curated pharmacology overlay (“fluconazole inhibits CYP2C9”, “warfarin is at toxicity risk”), never a bare variable or a raw transliterated name.

Belief revision

Nibli’s conclusions are never stored — they are re-derived from the current facts on every query. Retract a fact and everything that depended on it dissolves; nothing has to be manually un-concluded. This page covers the mechanics on both runtime surfaces.

Sources: GUARANTEES — Retraction Model, nibli-host REPL (nibli-host/src/main.rs), and the retraction metamorphic differential (nibli-verify/src/retract_diff.rs, part of just verify-soundness).

The guarantee: retract ≡ never-asserted

Retraction has one path — rebuild: the fact’s registry record is marked retracted and the knowledge base is rebuilt by replaying the surviving records. Equivalence classes, indexes, and the quantifier domain are all re-derived, so a KB after a retraction answers byte-identically to a fresh engine that never saw the fact.

This is not just documented — it is checked metamorphically at scale: the retraction differential generates seeded random programs mixing ground facts, rules, identity links, and stratified negation, retracts random earlier statements, and requires the engine to agree with a never-asserted twin on a battery of ground and quantified queries after every retraction.

In the host REPL

Facts get ids at assert time ([Fact #N] …, in file order under :load). List and retract by id:

:facts
[Facts] 24 active fact(s):
...

:retract 21
[Retract] Fact #21 retracted. KB rebuilt.

Re-query and the verdicts reflect the surviving facts only. With the durable store attached, the retraction persists as a tombstone — provenance is kept, and a replay never resurrects the fact.

Use :facts --all to inspect retained assertion records with active or withdrawn status. The default :facts still lists active statements only. Withdrawn records retain their ID and label across reopening a saved knowledge base; their obsolete payloads are not recompiled. This is retained assertion metadata, not a complete chronology of changes. :reset clears both sets.

A single assert_text call commits every root together or leaves the prior knowledge base unchanged. Separate input lines remain separate calls. A storage commit with an uncertain outcome retires the live session until the database is reopened, so subsequent queries cannot certify an uncertain state.

Two worked, engine-checked demos:

• GDPR walkthrough — withdraw consent (:retract 21): the lawful basis flips FALSE and the right to erasure flips TRUE.
• Drug-interactions walkthrough — discontinue the inhibitor (:retract 4) or the drug (:retract 10): the alert dissolves; in the second case the drug-level risk deliberately stays TRUE.

Verdicts that rest on an absence

Retraction interacts with negation-as-failure: a claim like “no lawful basis remains” becomes TRUE precisely because a search found nothing. The engine discloses this — such proofs carry the naf_dependent flag, and query results distinguish a deduced FALSE from UNKNOWN (naf-dependent) states. See What Nibli guarantees.

In the playground: edit and re-query

The browser playground has no :retract command — it does not need one. The nibli KR pane is the knowledge base, and every query rebuilds a fresh engine from that pane, so belief revision is edit-and-re-query: delete (or #-comment) the fact’s line, run the claim again, and the verdict reflects the edited KB. That is the same “retract ≡ never-asserted” semantics, achieved by construction.

The preset examples load read-only. To revise one, switch to Custom mode and paste the corpus in from the repo root (e.g. gdpr.nibli, drug-interactions.nibli — # comment lines are skipped at assert time), then comment out approves(Adam). or uses(Adam, Varfarin). and re-run the preset claims from the walkthroughs.

Authorization

Nibli ships a built-in authorization surface: a versioned KR policy, fail-closed vocabulary, and a warm Authorizer that answers with ordinary entailment. Allow means the engine returned TRUE for authorized(...) — not a learned score, not an LLM.

Code lives in nibli-auth (native), nibli:engine@0.12.0 authorizer (WASM component export), optional Rust features (axum, async-graphql, juniper), and nibli-auth-py / python/nibli_auth (PyO3).

This page is code-derived (crates, policy file, examples). It is not the Orange AVA book manuscript.

Ontology

Do not use as auth heads (corpus collisions):

Actions, roles, attrs are KR quoted strings: "read", "update", "admin", "title".

Entities (Agents & Resources) can be specified as:

• Capitalized Names: Alice, Doc1, User1
• Quoted Strings: "1", "2", "user_123" (required when IDs are numeric strings or lowercase).

owns(Alice, Doc1).                  # Capitalized name constants
owns("101", "202").                 # Quoted string IDs
authorized(Alice, "update", Doc1).   # query shape
has_role(Carol, "admin").
resource(Doc1).

Fail-Closed Lexicon & Custom Domain Roles (NIBLI_KR §13)

Nibli enforces a fail-closed vocabulary: uncurated predicate names (e.g., has_codename, program_role) are rejected at compile time rather than silently defaulting to an arity-2 guess. This prevents security bugs caused by typos (e.g., is_admim).

To model custom roles, permissions, or domain attributes without changing Rust code:

• Use has_role(Agent, "custom_permission_or_codename") with quoted string tokens (e.g., "read_application", "create_invoice"). Quoted string tokens can be any arbitrary string.
• Use in_tenant(Agent, "group_id") for custom tenancy/organization groups.

has_role(Alice, "read_application").
in_tenant(Alice, "org_sales_east").

Builtin policy

File: nibli-auth/policy/auth-0.1.0.nibli
Version constant: nibli_auth::POLICY_VERSION ("0.1.0").

Shipped rules (summary):

• Owner — owns($a, $r) ⇒ authorized for "read" and "update".
• Admin — has_role($a, "admin") & resource($r) ⇒ read/update that resource.
• Tenant — same tenant on agent and resource ⇒ "read" only.

Rule writing tip: every variable that appears in the conclusion should be constrained by a positive body condition (or bound by a ground query). Free conclusion-only variables do not fire under backward chaining here (admin rules therefore mention resource($r)).

Overlay extra KR with Authorizer::load_policy(Some(extra)) or per-call context_kr.

Efficiency model

Multi-threaded servers: the KB uses RefCell and is !Send. Do not put Authorizer in axum::State or Arc<Mutex<_>>. Use:

• Rust: nibli_auth::tls (thread-local warm policy).
• Python: same TLS behind nibli_auth_native (each OS thread warms once).

Cross-thread durable owns/roles belong in the app database and should be passed as context_kr each call (see the examples).

UNKNOWN on the hot path is treated as deny (allowed=false); only engine TRUE allows.

Rust API

#![allow(unused)]
fn main() {
use nibli_auth::{Authorizer, tls};

let mut auth = Authorizer::new();
auth.load_policy(None)?;
auth.assert_facts("owns(Alice, Doc1).")?;
let d = auth.can("Alice", "update", "Doc1", "")?;
assert!(d.allowed);

// Multi-thread / axum workers:
let d = tls::can("Alice", "read", "Doc1", "owns(Alice, Doc1).")?;
let batch = tls::can_any("Alice", "read", &["Doc1", "Doc2"], "owns(Alice, Doc1).")?;
let fields = tls::allowed_fields("Alice", "read", "Doc1", "owns(Alice, Doc1).", &["title", "body"])?;
}

• can — row-level allow/deny (Decision).
• can_any — batch queryset/row evaluation returning Vec<(String, bool)>.
• allowed_fields — v0.1: if row can allows, return all candidates (serializer masking).
• explain — same as can plus optional proof JSON.

Optional Cargo features on nibli-auth: axum (Agent header extractor, require, can_any, field_mask), async-graphql, juniper.

WIT (WASM component)

Package nibli:engine@0.12.0 exports authorizer alongside engine (logical auth surface v0.1 in the single shipping package).

Native and guest both wrap the same policy file via nibli-auth. engine.session and authorizer.session do not share a KB in v0.1.

Python API

just build-auth-py    # maturin develop into .venv-auth
just test-auth-py

from nibli_auth import can, can_any, allowed_fields, explain

d = can("Alice", "update", "Doc1", "owns(Alice, Doc1).")
assert d.allowed
results = can_any("Alice", "read", ["Doc1", "Doc2"], "owns(Alice, Doc1).")
fields = allowed_fields("Alice", "read", "Doc1", ["title", "body"], "owns(Alice, Doc1).")

Package layout: extension nibli_auth_native (PyO3); helpers under python/nibli_auth/ (fastapi_ext, optional drf, strawberry_ext, graphene_ext, spectacular).

Identity header in demos: X-Agent (not a production auth scheme).

Examples (same policy)

Scenarios: Alice owner, Bob stranger, Carol admin, Dave same-tenant read-only.

Extism

Extism is not the primary interface. A future PDK could wrap the same can / policy model; it is not implemented. Prefer the native Component Model / WIT path and in-process PyO3.

Versioning

Do not invent predicates outside the fail-closed lexicon. Bump the policy version string when shipping incompatible rule changes.

Tests

just test-auth          # Rust core + axum/graphql/juniper features
just check-auth-axum
just test-auth-py       # requires maturin / .venv-auth (also gated in CI: the auth-py job)
just docs               # includes this chapter

Developer guide — overview

Audience: contributors to the compiler, reasoner, host, and CI gates.

The engine is one deterministic pipeline — nibli-kr → nibli-semantics → nibli-reason — shipped four ways (native library, WASM component + Wasmtime host, and two browser bundles), with every guarantee backed by a runnable gate. The chapters:

• Crate map — the 22-crate workspace as a dependency graph: foundations, the compile chain, shared services, runtime surfaces, and tooling, with publish tiers.
• Pipeline & IR — how KR text becomes an AstBuffer, then the flat LogicBuffer FOL IR, and what shapes the compiler guarantees (the emitted-shape contract).
• WASM, host & compute — the single component, nibli-host mechanics (fuel, memory, trap recovery), the compute-backend protocol and its trust boundary, and the ship paths.
• Soundness & CI index — every gate: the two-oracle differential track, the six Lean proofs and their conformance bridges, the umbrella recipes, fuzzing and mutation testing.
• WIT surface — nibli:engine@0.12.0: every interface and session method, the bindings remap, and the version history.

Quick reference

Do not use the private book/ manuscript as a contributor reference for shipped behavior — prefer tests, gates, and the files above.

Crate map

The workspace has 22 member crates plus the deliberately excluded fuzz/ crate (root Cargo.toml: exclude = ["fuzz"]). Arrows below mean “depends on” (normal [dependencies] only — dev-dependencies are covered separately).

Two legibility omissions, disclosed: nibli-types edges are not drawn — most crates depend on it directly, and every crate except nibli-lexicon and lexigen at least transitively (nibli-store, nibli, nibli-auth-py, auth-axum, and fuzz reach it only through their deps) — and surfaces that wrap nibli-session also depend directly on the stage crates (nibli-kr / nibli-semantics / nibli-reason) for types and helpers — those direct edges are omitted where the session edge already implies the chain. Each crate’s Cargo.toml is the full truth.

flowchart TD
  subgraph foundations ["Foundations (dep-free)"]
    types["nibli-types<br/><i>canonical shared types</i>"]
    lexicon["nibli-lexicon<br/><i>committed English corpus</i>"]
  end

  subgraph chain ["Compile-and-reason chain"]
    kr["nibli-kr<br/><i>KR front-end (pest)</i>"]
    semantics["nibli-semantics<br/><i>AST → FOL LogicBuffer</i>"]
    reason["nibli-reason<br/><i>backward-chaining engine</i>"]
    session["nibli-session<br/><i>CoreSession — the ONE chain</i>"]
  end

  subgraph services ["Shared services"]
    protocol["nibli-protocol<br/><i>proof-trace wire format</i>"]
    render["nibli-render<br/><i>English rendering</i>"]
    store["nibli-store<br/><i>redb persistence</i>"]
  end

  subgraph runtimes ["Runtime surfaces"]
    engine["nibli-engine<br/><i>native embedding</i>"]
    pipeline["nibli-pipeline<br/><i>the WASM component</i>"]
    host["nibli-host<br/><i>Wasmtime host + REPL</i>"]
    wasm["nibli-wasm<br/><i>wasm-bindgen wrapper</i>"]
    ui["nibli-ui<br/><i>Dioxus playground</i>"]
  end

  subgraph tooling ["Tools, bins, extensions"]
    nibli["nibli<br/><i>6 dev bins incl. nibli-pin</i>"]
    import["nibli-import<br/><i>RDF/OWL import</i>"]
    formalize["nibli-formalize<br/><i>LLM English→KR gates</i>"]
    auth["nibli-auth<br/><i>logical authorization</i>"]
    authpy["nibli-auth-py<br/><i>PyO3 bindings</i>"]
    authaxum["auth-axum<br/><i>demo</i>"]
    verify["nibli-verify<br/><i>differential gates</i>"]
    lexigen["lexigen<br/><i>corpus refresh (report-only)</i>"]
    fuzz["nibli-fuzz<br/><i>3 libFuzzer targets</i>"]
  end

  kr --> lexicon
  semantics --> lexicon
  reason --> lexicon
  render --> protocol
  render --> lexicon
  session --> kr
  session --> semantics
  session --> reason
  store --> reason
  engine --> session
  engine --> store
  engine --> render
  engine --> protocol
  pipeline --> session
  pipeline --> auth
  host -. "loads nibli.wasm at runtime" .-> pipeline
  host --> kr
  host --> protocol
  host --> render
  host --> store
  wasm --> session
  wasm --> render
  wasm --> lexicon
  wasm --> protocol
  ui --> session
  ui --> formalize
  ui --> render
  ui --> lexicon
  ui --> protocol
  formalize --> kr
  formalize --> semantics
  formalize --> render
  formalize --> lexicon
  import --> engine
  nibli --> engine
  nibli --> import
  nibli --> render
  nibli --> kr
  auth --> session
  auth --> protocol
  authpy --> auth
  authaxum --> auth
  verify --> engine
  verify --> session
  verify --> lexicon
  lexigen --> lexicon
  fuzz --> engine
  fuzz --> kr
  fuzz --> semantics

The dashed edge is the one non-Cargo relationship in the graph: nibli-host does not link nibli-pipeline as a crate — it loads the built nibli.wasm component at runtime via Wasmtime (NIBLI_WASM_PATH).

Crate roster

Roles are taken from each crate’s own top-of-file doc comment. Tier is the crates.io publishing decision of record (RELEASING.md): Tier A is published to crates.io, in dependency order — see the API index for the live docs.rs links; Tier Z ships via GitHub Release / site / repo only.

Dev-dependency discipline

Several crates use the front-end as dev-dependencies only, keeping the release graph a strict DAG while letting tests build buffers the shipped way:

• nibli-kr dev-depends on nibli-semantics (golden tests: every emitted buffer must be accepted by the semantic compiler).
• nibli-reason dev-depends on nibli-kr + nibli-semantics (tests build event-decomposed LogicBuffers through the real front-end; the release build never links them).
• nibli-render dev-depends on nibli-kr + nibli-semantics for the same reason.

Where the boundaries are

• The one WASM boundary is host ↔ nibli-pipeline. Everything inside the component (nibli-kr → nibli-semantics → nibli-reason) is plain Rust function calls — see Pipeline & IR.
• Foundations are dependency-free by design: nibli-lexicon has zero dependencies; nibli-types only an optional serde.
• nibli-lexicon is the single arity source — nibli-semantics delegates to it instead of keeping a parallel arity map, and lexigen pins against the compiled corpus rather than parsing source.

Pipeline & logic IR

Normative reference: LOGIC_IR.md at the repo root — the public spec of the LogicBuffer IR. This page is the guided tour; the spec wins on any disagreement. The single source of truth for the types is nibli-types/src/logic.rs.

The pipeline

flowchart LR
  txt["nibli KR text"] -->|nibli-kr| ast["AstBuffer"]
  ast -->|nibli-semantics| lb["LogicBuffer (FOL IR)"]
  lb -->|nibli-reason| v["TRUE / FALSE / UNKNOWN<br/>+ ProofTrace"]
  lb -.-> tptp["TPTP → Vampire<br/>(nibli-verify)"]
  lb -.-> asp["ASP → clingo<br/>(nibli-verify)"]
  lb -.-> eng["English<br/>(nibli-render)"]

The three stages are plain Rust function calls — AstBuffer never crosses a WASM boundary, and nibli-semantics is an internal stage, not a component. The one WASM boundary is host ↔ nibli-pipeline, and only LogicBuffer (flat, u32-indexed, no pointers) crosses it. The LogicBuffer is the language-agnostic seam: only nibli-kr (parser) and nibli-lexicon (dictionary) are front-end-specific; the reasoner, both differential oracles, and the Lean proofs operate on or below the IR.

Queries and assertions use the same compiler — there is no separate query syntax at the IR level; divergence is entirely post-buffer. In particular, CountNode and executable ComputeNode formulas are evaluated only by query entry points when they occur in asserted position. Assertion and preassigned/replay entry points reject those uses before mutation because the store has neither a persistent cardinality-constraint representation nor a durable compute-evidence lifecycle. Either node inside an opaque abstraction body remains quoted content and is not evaluated against the outer KB.

CoreSession — the one compile chain

nibli_session::CoreSession packages the chain (nibli_kr::parse_checked → nibli_semantics::compile_from_ast → nibli_reason::transform_compute_nodes) plus the compute-predicate registry and the assert/query verbs. Every runtime surface — nibli-engine (native), nibli-pipeline (WASM component), nibli-wasm and nibli-ui (browser) — wraps it with only boundary conversion, so native↔WASM agreement holds by construction. Per-surface policy (error conversion, lint notes, env reads, persistence, compute-dispatch wiring) deliberately stays outside the core. The ordering is contractual: corpus name/arity resolution completes before compute marking. Registration is post-compile routing metadata for a corpus-resolvable relation, not a vocabulary or arity declaration; converted aliases and committed compounds normalize to their canonical IR relation.

AstBuffer (internal interchange)

The parser’s output and the semantic compiler’s input: parallel u32-indexed arrays (predicates / arguments / sentences / roots). It lives in nibli-types (not nibli-kr) because it is also nibli_kr::render’s input (the round-trip layer) and the validated programmatic-build target — hand-built buffers pass validate_ast_buffer (index bounds, acyclicity, the $-sigil invariant on variables) before compilation. Arguments are typed: Variable (sigiled $name), Marker (it / slot / ?), Pronoun (a closed 14-variant inventory), plus names, descriptions, numbers — there is no string-sniffed catch-all.

LogicBuffer (the FOL IR)

Two fields, no version field:

#![allow(unused)]
fn main() {
pub struct LogicBuffer {
    pub nodes: Vec<LogicNode>,
    pub roots: Vec<u32>,   // top-level formula nodes
}
}

13 LogicNode variants: Predicate, ComputeNode (an atom dispatched to the compute backend), AndNode, OrNode, NotNode, ExistsNode, ForAllNode, PastNode / PresentNode / FutureNode (tense), ObligatoryNode / PermittedNode (deontic), CountNode (“exactly N”). 5 LogicalTerm variants: Variable, Constant, Description, Unspecified, Number(f64). Spec and code match one-for-one in name, payload, and declaration order. Adding a variant is a breaking change across every conversion site; an in-source guard (__exhaustiveness_guard in logic.rs) forces that breakage to land in one documented location whose checklist names each site to update — including the ones no compiler error reaches (the WIT variant case + bindings regenerate, and the serde round-trip test).

Structural guarantees: post-order layout (children precede parents), DAG-not-tree (the flattener shares subtrees; acyclicity is the producer’s responsibility — the reasoner bounds-checks, it does not cycle-validate), and root granularity = fact granularity (split_roots() shares the whole node arena, exposing one root per fact). One footgun is flagged in both spec and code: CountNode’s middle field is a count, not a node index — the only non-index u32 payload in the IR.

There are deliberately no Biconditional/Xor nodes: the flattener expands A <-> B and A ⊕ B into And/Or/Not shapes (sharing subtrees) before the buffer exists.

Emitted-shape invariants (the contract)

These shapes are contract, not accident — pinned by the seam-conformance gate (just verify-nibli-kr-seam):

• Neo-Davidsonian event decomposition. dog(Adam). compiles to ∃ev. dog(ev) ∧ dog_x1(ev, adam) ∧ dog_x2(ev, Unspecified) — a unary type predicate over a fresh event variable plus one binary role predicate per dictionary place (dog is arity-2: x2 is the breed), unfilled places padded with Unspecified so role predicates stay arity-consistent.
• Quantifier shapes. some dog → Exists(v, And(restrictor, body)); every dog → ForAll(v, Or(Not(restrictor), body)) (the implication arrow); query-only exactly N → CountNode. Prenex all $x: … wraps the body directly — no restrictor, no arrow.
• Flavor-exact ordinary-predicate rule literals. PastNode / PresentNode / FutureNode remain attached to the antecedent or conclusion they wrap. Bare rule literals are Bare-only; the reasoner does not clone them into temporal flavors. A temporal mapping such as Past→Present therefore exists only when the KR rule declares both wrappers. Built-in identity and query-time compute dispatch keep their separately documented semantics. One formula path may carry one temporal or one deontic wrapper, never both: KR rejects mixed prefixes, AST compilation/rendering rejects dual-field propositions, and the reasoner rejects manually nested raw IR before assertion, query/find, proof construction, materialisation, or replay. Separate rule literals may still carry different wrappers.
• Flat-atom families. Not everything is event-decomposed: equals (the identity) stays a flat 2-argument atom (the union-find ingests exactly that shape); via modal tags, the the_domain_<name> restrictors, and the abstraction type predicates are also flat.
• Abstraction opacity. event { P() } bodies compile behind a versioned __abs_v1_<digest>_<key> marker. The tagged, length-delimited, alpha-canonical key contains abstraction kind + body and is the lossless identity; the digest is a non-semantic readable prefix recomputed from the key at every assert/query ingress. Malformed/unknown marker versions fail closed, and exact goldens freeze the v1 byte layout. The reasoner matches the complete marker but skips the body, so asserting believe(me, fact { P }) never makes bare P true.
• Compute transform. The front-end never emits ComputeNode; nibli_reason::transform_compute_nodes rewrites marked Predicates after fail-closed corpus compilation. The registry cannot make an unknown text name compile or supply its arity. A BYO-buffer producer may run the transform over its own exact IR-name set, or construct a raw ComputeNode directly; a compute relation left as a plain Predicate is treated as an ordinary fact.

NotNode is structurally plain ¬ — the closed-world reading is a reasoner property, carried on the verdict side by ProofTrace.naf_dependent and ProofTrace.cwa_false.

Entry points

The reasoner’s fact store remains a set keyed only by StoredFact; origin is a separate structural support index. Every insertion records a direct assertion, forward derivation with grounded premises, existential-import presupposition, or explicit internal source. Rule citations use the full collision-safe rule identity internally and expose the source assertion id plus deterministic local ordinal. Rebuild/reopen regenerate both indexes from active LogicBuffers, so the disposable typed mirror never becomes provenance authority.

Stable vs internal

Stable: the 13+5 variant inventories (names, payloads, declaration order); the two-field buffer; post-order layout; root granularity + split_roots; the emitted-shape invariants; the ProofRule/ProofStep/ProofTrace JSON contract; the NibliError display prefixes; the WIT logic-types interface.

Internal: variable/Skolem naming (_v0, sk_N), the exact versioned __abs_ payload, concrete index values, the compiler’s tree IR (IrForm), stored-fact forms, on-disk mirrors.

The buffer has no version field — the WIT package version (nibli:engine@0.12.0) and nibli-store’s fail-closed schema versions are the only version markers. Treat the format as pre-1.0: pin a commit if you build against it.

Writing a consumer or producer

The two shipped external consumers are the templates: nibli-verify/src/tptp.rs (→ Vampire; hard-errors on out-of-fragment nodes rather than mistranslating) and nibli-verify/src/asp.rs (→ clingo; regroups the event decomposition back to surface atoms). A producer must emit the invariant shapes — most importantly the event decomposition with consistent role arities, the ∀-implication arrow, and flat 2-arg equals — and gets soundness checking for free: the reasoner rejects non-stratifiable rule sets at assert time.

WASM, host & compute

How the engine ships: one WASM component, a native Wasmtime host, an optional external compute backend, and two browser surfaces that skip WASI entirely.

Sources: nibli-host/src/main.rs, nibli-protocol/src/compute_client.rs, python/nibli_backend.py, DEPLOY.md.

One component, four runtimes

nibli-pipeline is the single WASM component (WIT world nibli-pipeline): nibli-kr / nibli-semantics / nibli-reason are internal Rust crate dependencies, not separate components. It imports compute-backend from the host and exports the engine + authorizer interfaces (WIT surface).

All four wrap the same nibli_session::CoreSession, so they agree by construction. The dispatch hook is per-KB-instance function pointers (KnowledgeBase::set_compute_dispatch) — nibli-reason itself holds no thread-locals or globals, which is what lets multithreaded embedders register it at all. The native TCP client those pointers call into does live per-thread in the embedder (nibli-engine/src/compute_client.rs), so a multithreaded native embedder calls enable_compute_backend on each worker thread that reasons.

nibli-host mechanics

just run builds the component and launches the host (NIBLI_WASM_PATH=target/wasm32-wasip2/debug/nibli.wasm by default).

Environment variables (read at startup):

Runtime toggles: :depth [n], :fuel [n], :memory [mb], :backend [addr], :strict on|off, :existential-import on|off, :materialize on|off (bare :materialize prints the saturation report). Script mode (--script <file> or piped stdin) captures transcripts byte-faithfully.

The host prints the effective existential-import profile at startup and after a toggle. Changing it is a fallible transactional replay of the active assertion registry, so existing universals gain or lose imported witnesses immediately; find/proof/count results carry structured import provenance. The browser UI labels the same clean-core vs legacy-import profile.

Resource traps don’t brick the session. Fuel exhaustion (wasmtime::Trap::OutOfFuel) and memory-grow denials are classified and — for queries — synthesized into a RESOURCE_EXCEEDED (fuel|memory) verdict with a remediation hint. A trap poisons the component instance, so the host keeps a journal of every successful KB mutation and lazily rebuilds a byte-identical session on the next call (the engine is deterministic: identical fact ids and Skolem numbering). The journal records successful strict, import and depth changes in order. A replacement component is published only after complete replay. Failed replay leaves the session unavailable; raising :fuel or :memory lets the next dependent command retry once. An uncertain durable commit requires reopening the saved database. Depth limits are engine-level, never a trap.

The compute backend

An external process the reasoner can consult for computed predicates — JSON Lines over TCP, one object per line:

{"relation": "exponential", "args": [{"type": "number", "value": 8.0}, {"type": "number", "value": 2.0}, {"type": "number", "value": 3.0}]}
{"result": true}

Responses are {"result": true|false} or {"error": "..."}. Argument tags: variable, constant, description, unspecified, number.

• Built-in vs forwarded: product / sum / quotient with fully numeric arguments evaluate locally (the shared nibli_types::eval_arithmetic); a call whose arguments don’t resolve to numbers falls through to the backend — which is why the reference server implements all three too. Any other corpus relation successfully registered via :compute <name> forwards. Registration normalizes aliases and committed compounds to their canonical compiled relation and is refused while live stored facts or rules reference that relation (retract first); bare :compute reports the canonical registry.
• Text name boundary: registration runs after fail-closed KR compilation. It does not declare vocabulary or infer arity, so an unknown name is refused and remains an unknown text predicate. Native BYO-IR callers can query an arbitrary relation by constructing ComputeNode(name, args) directly—its argument vector supplies the raw shape and no registration is needed. The shipping component exposes no raw-buffer query or vocabulary/schema method; implementing compute-backend or adding a server handler alone cannot add a component text predicate.
• Tolerant equality (disclosed): arithmetic equality is isclose with rel_tol 1e-9, abs_tol 0 — 0.3 = 0.1 + 0.2 is TRUE. The comparison predicate num_equal is exact ==. Non-finite operands yield UNKNOWN (non-finite); find/count/aggregate then refuse the incomplete collection rather than return empty/zero/None.
• Comparisons are query-only, and that is decided: greater / less / num_equal over operands that could be numbers are refused at assertion ingress in facts and in every rule position, so there is no numeric threshold rule. On the query side they decide a verdict and also filter witnesses in find / count_witnesses / aggregate.
• Witness enumeration never dispatches: find / count_witnesses / aggregate run the same group recogniser the verdict path does, so anything definitively decidable locally — a comparison, or finite built-in arithmetic over resolved operands — filters rows. A locally detected non-finite operand or overflow is also non-definitive and makes the collection incomplete. Anything whose routing would reach the backend is refused at the dispatch choke point with a budget of ZERO calls, and the enumeration is reported incomplete. Any final UNKNOWN or RESOURCE_EXCEEDED leaf has the same complete-or-error collection behavior. UNKNOWN (backend-unavailable) there means the engine declined to call out, not that the backend failed.
• Admission policy (explicitly low-assurance): an external reply is trusted evidence for the current ComputeCheck. The stock client is plaintext and unauthenticated, with no peer identity, confidentiality, integrity or request/response ID, protocol/backend/schema version, nonce/timestamp, freshness/expiry, replay/revocation check, or admission receipt. Scalar replies bind to the next line and batch replies bind by input order. Any parseable Boolean is trusted, so a valid forged, replayed, stale, reordered, or revoked-peer reply is not detectable. Use the stock path only on loopback or a segment whose backend and path the operator accepts as TCB.
• Custom admission: native embedders can replace the client with NibliEngine::set_compute_dispatch; component embedders can implement the WIT compute-backend import; an operator can also supply an external secured transport. The stock nibli-host has no admission plug-in—:backend and NIBLI_COMPUTE_ADDR select only an address. A rejected custom call becomes UNKNOWN (backend-unavailable), and the current proof schema cannot carry an identity, wire transcript, timestamp/nonce, or policy receipt. This is an admission hook, not a guest vocabulary/schema hook.
• Proof-local lifecycle: built-in and external results are never inserted into the typed fact store or assertion registry. They receive no fact id, do not appear in :facts, cannot be retracted, never change the quantifier domain, are not persisted or journaled, and trigger no forward chaining. Compute atoms are query-only: executable ComputeNodes in assertions or any rule position fail before id allocation — as are the reference external names (exponential/logarithm) even when unregistered, so registration order cannot strand a stored fact; opaque abstraction bodies remain quoted. Each top-level query recomputes or redispatches. Repeated identical external checks may share a transient within-query memo to keep the verdict and trace consistent; the memo never survives into another query. Compiled KR and raw flat ComputeNode buffers follow the same lifecycle, although only the native raw-IR path can name a relation outside the text corpus.
• No backend configured? A registered external predicate answers UNKNOWN (backend-unavailable) — an outage is never a derived falsehood (pinned by the smoke-host-backend-unavailable gate). The result remains UNKNOWN after an earlier success and despite any matching ordinary fact; there is no compute-result outage cache or fact-store fallback.
• Opaque generated argument? Internal Skolem/SkolemFn identity has no lossless representation in this string-only protocol. Dispatch therefore fails closed as UNKNOWN (backend-unavailable) before the host callback runs. A user constant whose literal text is sk_0 is not internal and is forwarded.
• Client behavior: lazy connect, reused connection (idle reap after 300 s, read timeout 10 s, write 5 s — NIBLI_BACKEND_* env overrides), and a batch path that pipelines requests and associates replies by order. Scalar dispatch drops the connection and retries once after any failed attempt; batch dispatch retries the whole batch after a connect/write/read failure. Because a first write or partial batch may already have executed, stock backends must be pure and idempotent; custom scalar/batch dispatchers must also agree on ordering and cardinality.

The reference server is python/nibli_backend.py (just backend, port 5555): handlers product, sum, quotient, exponential, logarithm in a HANDLERS dict. Adding a handler extends what the transport can answer; it does not add a KR text name. A new arbitrary name additionally requires a native raw ComputeNode query today, or a future explicit vocabulary/schema extension. just run-with-backend wires host + backend together.

Browser surfaces

No WASI, no component, no server: nibli-wasm (wasm-bindgen Session for JS; powers the live demo) and nibli-ui (the Dioxus playground) compile the engine crates straight into the browser bundle. nibli-wasm keeps two deprecated no-op shims (set_language, back_translate) for deployed-site compatibility until the site migration lands; the live back-translation is IR-driven (back_translate_ir).

Ship paths

just build-ui produces the exact shipping bundle locally (target/dx/nibli-ui/release/web/public/) as a pre-merge sanity check — the production build runs in the site repo. Since the committed corpus, no build needs a dictionary fetch — the full vocabulary is compiled in (the site repo’s leftover fetch step is obsolete and unread; see DEPLOY.md).

Soundness & CI index

Every guarantee in GUARANTEES.md is backed by a gate you can run. This page indexes them: what each gate checks, what it needs, and when it runs. The Justfile is the source of truth for recipe contents.

The umbrella recipes

GitHub Actions (.github/workflows/ci.yml) runs four parallel jobs, all inside the Nix shell: runtime-ci (just build-wasm — bindings are generated, gitignored, absent on fresh checkouts — then just ci-all), auth (just test-auth + check-auth-axum), docs (just docs), and fuzz (just fuzz-ci, time-boxed).

The verify-* gates

Track A proper is the differential-oracle family (the first row); the rest are supporting native gates that ride the same ci umbrella.

Determinism is a three-way gate: the same pinned corpus (determinism-corpus.nibli) must produce identical verdicts on the native engine (in verify-nibli-kr-seam), the Wasmtime component (smoke-host-determinism), and node/V8 (verify-wasm-node, skips without wasm-pack) — the browser-class runtime of the live playground.

Track B — mechanized proofs

Six Lean 4 proofs in proofs/ (no mathlib — self-contained, offline), checked by just verify-proofs (skips cleanly without lean; the Nix shell provides it). Each proof is bridged to the real engine by a Rust conformance test that runs even when Lean skips:

Honest scope (stated in proofs/README.md and GUARANTEES): the proofs are model-level plus corpus conformance tests — not one end-to-end machine-checked pipeline from source text to model. The KR→semantics seam is conformance-gated (the seam gate), which narrows but does not close that gap.

On-demand gates

Reading GUARANTEES.md

The contract document is organized as: Front-End Language, Soundness (Tracks A + B, the seam gate, the mutation baseline, determinism), Completeness, Negation Policy, Equality Semantics, Predicate Validation, Integrity Constraints, Resource Limits, Retraction Model, Query Result Contract, Hypothetical Reasoning, Aggregation, Disclosed Sharp Edges, What the Engine Cannot Do, Closed Base Vocabulary, and Time and Order. Its core statement: if the engine says TRUE, a formal derivation from your asserted facts and rules exists — and the proof trace shows it.

WIT surface

The component boundary, as declared in wit/world.wit — package nibli:engine@0.12.0, world nibli-pipeline:

world nibli-pipeline {
    import compute-backend;
    export engine;
    export authorizer;
}

One component, one world. The WIT package version is independent of crate semver (a locked decision of record). Only flat, u32-indexed data crosses the boundary — no heap pointers.

Interfaces

error-types

variant nibli-error identifies the pipeline stage that failed: syntax(syntax-detail) (with message + 1-based line/column), semantic(string), reasoning(string), backend(tuple<string, string>).

logic-types

The IR and verdict types (Pipeline & IR):

• logical-term (5 cases) and logic-node (13 cases) mirror nibli_types::logic exactly — kebab-case names, identical declaration order (the component-model discriminant is positional).
• logic-buffer { nodes, roots }.
• count-node remains part of the shared formula IR for query/proof input. Assertion and replay methods reject it in asserted position, while opaque abstraction content remains quoted; the WIT has no persistent cardinality-constraint type.
• query-result: true | false | unknown(unknown-reason) | resource-exceeded(resource-kind), with unknown-reason ∈ {cycle-cut, incomplete-knowledge, naf-dependent, backend-unavailable, non-finite} and resource-kind ∈ {depth, fuel, memory}.
• witness-origin: knowledge-base | generated-witness | existential-import; witness-binding { variable, term, origin }, fact-id (u64), fact-summary { id, label, root-count }.
• proof-rule (20 cases) + 16 named-field payload records (WIT variant cases hold at most one payload type, so each data-carrying case gets a record — the interface self-documents instead of using positional tuples); exists-witness-rule carries origin, while count-result-rule carries existential-imported alongside expected and actual. asserted-rule lists every active assertion citation, derived-rule lists stable assertion-local rule citations, and presupposed-rule keeps existential-import evidence distinct from user-given facts; proof-step { rule, holds, children }; proof-trace { steps, root, naf-dependent, cwa-false } — the NAF/CWA flags are computed once in the engine and carried across so consumers never recompute them.
• materialization-report { complete, refused } — cumulative requested query cones since the last KB mutation: completed relations and one-line refusal reasons. It may remain empty when an exact positive proof needed no saturation.

compute-backend (the host import)

• evaluate(relation, args) -> result<bool, nibli-error>
• evaluate-batch(requests) -> list<compute-result> — one boundary crossing for N requests; results in input order, one failure never poisons the batch.

The engine calls this for predicates registered for compute dispatch; the host answers built-in arithmetic locally and forwards the rest over TCP (WASM, host & compute).

The import transports relation calls; it does not declare guest KR vocabulary or arity. The exported session resolves text through the committed corpus before compute marking, and this WIT version has neither a raw-buffer query nor a vocabulary/schema method. A custom host implementation therefore cannot make an arbitrary relation name usable through query-text merely by accepting it.

Results are query-local. Neither evaluate nor evaluate-batch creates a KB fact, fact id, registry row, or replay entry, and a later backend error is UNKNOWN (backend-unavailable) even if the same request succeeded earlier.

This import is also the component’s admission boundary. The WIT contract is transport-neutral and carries relation, arguments, and Boolean/error results—not peer identity, signatures, request IDs, versions, timestamps/nonces, or policy receipts. The component trusts an ok(bool) from its host. The stock nibli-host implementation forwards over deliberately unauthenticated JSONL/TCP; a custom host may authenticate or otherwise admit calls before returning, but its policy metadata is outside the current proof schema.

engine (export) — the session resource

authorizer (export)

The built-in authorization surface (logical auth v0.1), wrapping the same policy as the native nibli-auth crate. Types: decision { allowed, verdict, reason, fields } (allowed is true only on entailment TRUE) and explained { decision, proof-json }. Session methods: load-policy, assert-facts, retract, can, can-any (batch), allowed-fields, explain, policy-version, clear-ephemeral. Two conventions worth knowing: the protected-resource parameter is named object (WIT reserves the keyword resource), and error results are plain string, not nibli-error.

Bindings: the types ARE nibli_types

nibli-pipeline is the only crate with WIT bindings, regenerated by cargo component build -p nibli-pipeline (the just build-wasm recipe, which also cargo fmts the output; src/bindings.rs is gitignored — CI regenerates it on every run).

[package.metadata.component.bindings.with] remaps the eleven ABI-matching boundary types onto the canonical nibli_types definitions — logical-term, logic-node, logic-buffer, query-result, unknown-reason, resource-kind, witness-origin, witness-binding, fact-summary, assertion-status, assertion-record-summary from logic-types, plus nibli-error and syntax-detail from error-types — so the guest passes the canonical types straight through instead of maintaining a mirror-conversion layer.

The one exception is the proof trio: proof-rule is named-field in Rust but wit-bindgen emits only tuple/newtype variants, so it keeps the single hand-written convert_proof_rule bridge in nibli-pipeline/src/lib.rs (proof-step/proof-trace reference it and stay generated too).

Version-bump checklist: the remap keys pin the interface version (nibli:engine/logic-types@0.12.0/…). Any WIT version change must bump all thirteen keys — a missed key silently stops remapping and resurrects the mirror types.

Version history

The 2026-08-13 text-contract reconciliation narrowed registration to existing corpus relations without changing these WIT method shapes or the 0.11.0 package ABI. The table records when each ABI member was introduced, not every later semantic clarification.

Engine specifications

Normative and operational specs live at the repository root (and in-tree sources). This page is a link-out index — not a second copy of those files.

API documentation

Rust crate APIs are on docs.rs — every published crate is listed with its versioned link in the API index, starting from docs.rs/nibli-engine. From a checkout, cargo doc -p <crate> --open builds the same rustdoc locally. That is separate from this mdBook site, which carries the conceptual docs only.

Hosting note

API index

Rustdoc for the embeddable crates, on docs.rs since the first publish (v0.1.0, 2026-08-03). Embedding starts with one line:

cargo add nibli-engine

Every crate below is version 0.1.0 in workspace lockstep, MIT OR Apache-2.0, published in the dependency order the Tier A/Z decision table in RELEASING.md locks. (docs.rs builds each crate shortly after publish — a page may briefly show “building” right after a release.) For local API docs from a checkout, cargo doc -p <crate> --open still works.

Publishable crates (Tier A, in dependency order)

Not on the list

The Tier Z crates (nibli-pipeline, nibli-host, nibli-ui, nibli-wasm, nibli-verify, nibli-lexigen, plus the workspace-excluded fuzz/ harness) are publish = false: they ship as the WASM component, host binary, hosted sites, and CI gates rather than as libraries — the v0.1.0 GitHub Release carries the built component and host. Their internals are covered by the developer guide. The auth crates (nibli-auth, nibli-auth-py) and the auth-axum example are also publish = false for now — they sit in neither tier row of the decision table; the authorization guide covers their APIs.

Conceptual documentation (this site) stays on the primary/mirror hosts only — docs.rs carries API docs, not these pages.