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, given a correct implementation. 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.

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.

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.

Trusted compute backend

Results from the external compute backend (exponential, logarithm, or predicates you register) are a trusted oracle, not a derivation: a true reply is auto-asserted mid-query. Built-in arithmetic (product / sum / quotient) is local. Any conclusion that passes through the backend is only as sound as that oracle.

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

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).

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).

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 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 ground numeric comparisons work locally. External compute backend predicates need the host + backend path (just run-with-backend) — not the pure playground.

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:

obligated_by(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.

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.7.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.7.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 (local)
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.7.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.

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.

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); exactly N → CountNode. Prenex all $x: … wraps the body directly — no restrictor, no arrow.
• 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 content-hashed __abs_<hash> marker: the reasoner matches the 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 compilation. BYO-buffer users must run it themselves — 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

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), __abs_ hash digits, 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.7.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: :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.

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). Raising :fuel between trap and re-query applies to the replay. 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. Everything else registered via :compute <name> forwards.
• 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).
• Trust boundary (disclosed): a backend true reply is auto-asserted as a ground fact mid-query which downstream rules chain on. The backend is part of the trusted computing base — a plaintext, unauthenticated peer; run it on localhost or a segment you control. Auto-asserted compute facts are non-durable — never journaled or replayed, recomputed on demand, and they do not survive a restart (the persistent engine’s typed mirror is cleared and rebuilt from the fact registry on open).
• 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).
• Client behavior: lazy connect, reused connection (idle reap after 300 s, read timeout 10 s, write 5 s — NIBLI_BACKEND_* env overrides), retry-once on connection errors, and a batch path that pipelines all requests in one burst to amortize WASM-boundary and TCP round trips.

The reference server is python/nibli_backend.py (just backend, port 5555): handlers product, sum, quotient, exponential, logarithm in a HANDLERS dict — extend by adding an entry. 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.7.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 }.
• 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-binding { variable, term }, fact-id (u64), fact-summary { id, label, root-count }.
• proof-rule (19 cases) + 15 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); 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 } — which relations the NAF saturation completed, and which it refused with a one-line reason each.

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).

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 ten ABI-matching boundary types onto the canonical nibli_types definitions — logical-term, logic-node, logic-buffer, query-result, unknown-reason, resource-kind, witness-binding, fact-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.7.0/…). Any WIT version change must bump all ten keys — a missed key silently stops remapping and resurrects the mirror types.

Version history

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.