nibli-render 0.1.0

Shared human-readable rendering for the Transparency Triad back-translation and proof traces
Documentation

Nibli

Release crates.io Docs

A zero-hallucination symbolic reasoning engine.

Nibli is a deterministic theorem prover compiled to WebAssembly (WASI P2). It compiles nibli KR — a human-readable predicate-call knowledge-representation language (dog(Adam)., animal(every dog).) — into First-Order Logic and performs inference via demand-driven backward chaining over an indexed fact store. Every conclusion is a formal derivation — never a guess, never a generated step. (Lojban, nibli's original surface syntax, retired at THE DROP — the last dual-front-end engine is tagged v0.1-lojban-final, and the Lojban tooling was donated to a separate repo.)

nibli (Lojban): x1 logically entails x2 under rules x3

What "zero-hallucination" means here

Nibli derives every conclusion from the facts and rules you assert, under two explicit assumptions:

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

Results from the external compute backend (exponential, logarithm, or any predicate you register) are a trusted oracle, not a derivation: a true reply is auto-asserted into the knowledge base as a ground fact mid-query, and downstream rules chain on it as if you had asserted it yourself. The backend is part of the trusted computing base — an axiom source — so any conclusion that passes through it is only as sound as that oracle. (Built-in arithmetic, product/sum/quotient, is computed locally — see Compute Backend.) So a verdict reads as:

  • TRUE — a proof exists from those premises (your facts + rules + trusted backend results).
  • FALSE — not derivable from those premises. This is not a proof of ¬P.
  • UNKNOWN — the search could not decide: a cycle, incomplete knowledge, or a negation over an undecided sub-goal.

The guarantee is soundness relative to what you asserted, not omniscience — change the premises and the verdict can change. What Nibli rules out is fabrication: it never invents a fact, a rule, or a proof step.

The nibli KR Language

nibli KR is a strict predicate-call surface for first-order claims: intuitive to read, but every semantic distinction stays visible in the spelling (the anti-silent-mistranslation design rule). 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 (~1,342 strongly-typed predicate entries, every place named), fail-closed; a+b compounds resolve only via committed compound entries.

nibli KR Reads as
dog(Adam). Adam is a dog
animal(every dog). every dog is an animal (a rule)
~eats(Adam). Adam does not eat
past eats(me, some food). I ate some food
dog(Adam) & cat(Betis). conjunction (| or, -> if-then)
goes(Adam, destination: some market). named argument places, Python-style
beautiful(every person where ~cat). rule with a negated restrictor (negation-as-failure)
Kim = Adam. identity — Kim and Adam are the same individual
red(exactly 2 red). exact-count claim
runs(some [big dog]). compound predicate: a big-dog kind of runner
desires(desired: every teaches, desirer: event { studies() }). event abstraction
all $x: dangerous($x) & uses(Adam, $x) -> warns($x). explicit prenex rule with variables

The normative spec is NIBLI_KR.md (v0.1 compat profile, implemented); the executable grammar is nibli-kr/src/nibli_kr.pest — the parser is generated from it, so the spec and the parser cannot drift. The front-end's independent oracle is the KR seam gate (verify-nibli-kr-seam: hand-verified FOL structural goldens + a construct-inventory sweep + metamorphic relations, in CI).

Pipeline

nibli KR text ──> Front-end (nibli-kr) ──> Semantic Compiler (FOL IR) ──> Reasoning Engine
                        │                                   │                            │
              pest grammar → AST buffer               Skolemization              Backward chaining
             (fail-closed name resolution)          + event semantics         over indexed fact store

Both front-ends emit the same flat AST buffer, so everything downstream is shared. The pipeline stages are linked as internal Rust crate dependencies and compiled into a single WASM component:

Crate Name origin Role
nibli-kr — nibli KR text → AST → flat WIT buffer (pest grammar + fail-closed alias resolution + the canonical renderer)
nibli-semantics — AST buffer → FOL logic IR → flat WIT logic buffer
nibli-reason — FOL logic buffer → backward-chaining assertion, query, and proof
nibli-pipeline — Orchestrator: chains the front-end → nibli-semantics → nibli-reason into a single WASM component
nibli-host — Native Wasmtime host, REPL, and TCP compute backend client

Supporting crates:

Crate Role
nibli-lexicon The committed English corpus — strongly-typed predicate + compound entries (name, named places, gloss, template, gismu provenance), const-validated; the single vocabulary source for every stage
nibli-engine Native in-process embedding of the pipeline (used by tests and the store layer)
nibli-ui Standalone Dioxus web UI — the engine is compiled in and runs fully in-browser
nibli-wasm wasm-bindgen wrapper exposing the in-browser pipeline (powers the live demo)
nibli Native debug REPL and nibli-validate tooling

The FOL IR in the middle of the pipeline — the LogicBuffer — is nibli's language-agnostic seam and is publicly specified in LOGIC_IR.md (node types, flat-buffer layout, emitted-shape invariants, stable-vs-internal surface, and the entry points for building alternative front-ends or consumers against it).

Runtime Surfaces

Canonical entrypoints:

  • nibli-host — Local REPL and operator runtime for the theorem prover. The main single-node runtime. Use just run.
  • nibli-ui — Standalone browser frontend (Dioxus). The engine is compiled into the WASM bundle and runs fully in-browser — no server. Use just ui.

Supporting surfaces:

  • nibli-engine — Shared native embedding library. Not a user-facing runtime.
  • nibli-wasm — wasm-bindgen wrapper exposing the in-browser pipeline (powers the live demo at dhilipsiva.dev/nibli).
  • nibli — Native direct-crate REPL and nibli-validate. Developer tooling, not the canonical production path.

Every surface speaks nibli KR — the single front-end since THE DROP.

Documentation

Code-derived human docs live in mdbook/ (mdBook). They are not the Orange AVA book manuscript (book/ is a separate, private checkout).

Surface How
Live mirror https://dhilipsiva.github.io/nibli/
Local just docs / just docs-serve (http://127.0.0.1:3000) inside nix develop
Primary (site integration) https://dhilipsiva.dev/docs/nibli/ — see DEPLOY.md
Playground https://dhilipsiva.dev/nibli-playground/
Rust API cargo doc -p <crate> --open — docs.rs when crates are published
Roadmap DOCS_TODO.md

Root specs remain canonical: NIBLI_KR.md, LOGIC_IR.md, GUARANTEES.md.

Authorization

Built-in, zero-hallucination authorization (entailment of authorized(...) under a versioned KR policy):

Piece Location
Guide mdBook: Authorization (or just docs-serve)
Rust crate nibli-auth — Authorizer, tls (thread-local for async servers)
WIT nibli:engine@0.6.0 export authorizer
Python just build-auth-py → nibli_auth / nibli_auth_native
Examples examples/auth-axum, examples/auth-fastapi (same policy)
Tests just test-auth; Python: just test-auth-py (local, maturin)

Policy file: nibli-auth/policy/auth-0.1.0.nibli. Extism is not the primary interface (optional future PDK only).

Getting Started

Prerequisites

  • Nix (all tools — rustc, cargo-component, just, wasmtime — come from flake.nix)

Build and Run

# Enter the dev shell
nix --extra-experimental-features 'nix-command flakes' develop

# Build all components and launch the REPL
just run

# Run all unit tests
just test

Dictionary data. The dictionary is COMMITTED Rust source: nibli-lexicon/src/corpus/ holds ~1,342 strongly-typed predicate entries (every place named in English; arity = places.len() by construction) plus curated a+b compound entries, derived from the lensisku Lojban dictionary (jbovlaste data, CC-BY-SA) and const-validated on every compile. There is ONE build mode — no JSON is read at build time, so just run/just test, CI, and the deployed site all carry the identical full vocabulary, fully offline. dictionary-en.json (gitignored; just fetch-dict) is only the input of the tools/lexigen regeneration tool (just regen-lexicon), which reports drift and candidate new entries but never rewrites committed rows.

REPL Usage

~/nibli> big(some dog).
[Skolem] 3 variable(s) → _ev0 ↦ sk_2, _ev1 ↦ sk_1, _v0 ↦ sk_0
[Fact #0] Asserted.

~/nibli> animal(every dog).
[Skolem] 2 variable(s) → _ev0 ↦ sk_4(∀-dependent), _ev1 ↦ sk_3(∀-dependent)
[Rule] Compiled ∀_v0 to backward-chaining rule
[Fact #1] Asserted.

~/nibli> dog(Adam).
[Skolem] 1 variable(s) → _ev0 ↦ sk_7
[Fact #2] Asserted.

~/nibli> ? animal(Adam).
[Query] TRUE
[Why] Because adam is a dog, adam is an animal.
  ⊢ adam is an animal  [by the rule: every dog is an animal] -> TRUE
    ▣ adam is a dog  [given] -> TRUE

~/nibli> ?? dog($x).
[Find] _ev0 = sk_7, $x = adam
[Find] _ev0 = sk_1, $x = sk_0

~/nibli> :debug big(exactly 2 dog).
[Logic]
Count _v0 = 2:
  And:
    ∃ _ev1:
      And:
        And:
          dog(_ev1)
          dog_x1(_ev1, _v0)
        dog_x2(_ev1, something)
    ∃ _ev0:
      And:
        And:
          And:
            big(_ev0)
            big_x1(_ev0, _v0)
          big_x2(_ev0, something)
        big_x3(_ev0, something)

[English] Exactly 2 things are such that X is a dog and X is big.

~/nibli> :assert exponential 8 2 3
[Skolem] 1 variable(s) → _ev0 ↦ sk_8
[Fact #3] exponential(8, 2, 3) asserted.

~/nibli> :facts
[Facts] 4 active fact(s):
  #0: big(some dog). (1 root)
  #1: animal(every dog). (1 root)
  #2: dog(Adam). (1 root)
  #3: :assert exponential (1 root)

~/nibli> :retract 1
[Retract] Fact #1 retracted. KB rebuilt.

~/nibli> :load readme.nibli
[Fact #4] logical system(Nibli).
[Fact #5] certain system(Nibli).
...
[Load] Done: 71 asserted, 37 skipped, 4 errors

~/nibli> :reset
[Reset] Knowledge base cleared.

(The :debug view exposes the formal event-decomposed IR: nibli KR's dog/big compile to the English predicates dog/big plus their role predicates dog_x1/big_x2/… — no Lojban. The 4 :load errors are deliberate fail-closed rejections — bare negations and one non-flat rule conclusion ingest no facts rather than being silently misreported as asserted.)

Query results use a four-valued contract: TRUE, FALSE, UNKNOWN (with reason: cycle cut, incomplete knowledge, NAF dependence, backend unavailable, or non-finite numeric), or RESOURCE_EXCEEDED (depth, fuel, or memory limit hit). The engine never guesses.

You query by stating the proposition you want checked, not by asking a question. ? animal(Adam). reads "is Adam is an animal entailed?" — and the verdict is the answer. The engine has no interrogative form: state animal(Adam). ("Adam is an animal"), never "Is Adam an animal?". The ? prefix marks the line as a query; it is not a question mark on the claim.

REPL Commands

Command Description
<statement> Assert a statement (nibli KR) as a fact or rule
? <statement> Query with proof trace
?? <statement> Witness extraction (find all satisfying bindings, $x variables)
:debug <statement> Show compiled FOL logic
:assert <rel> <args...> Assert a fact directly (bypasses text parsing)
:retract <id> Retract a fact by ID and rebuild the KB
:facts List all active facts
:load <filepath> Batch-load a .nibli file
:reset Clear the entire knowledge base
:compute <predicate> Register a predicate for external compute dispatch
:backend [host:port] Show or change the compute backend address
:fuel [amount] Show or set the WASM fuel limit
:memory [mb] Show or set the WASM memory limit
:strict [on|off] Show or set strict mode — reject arity/constraint violations instead of warn-and-insert (also NIBLI_STRICT=1)
:existential-import [on|off] Show or set xorlo witness minting (default ON) — off is the clean-core profile where a description universal (animal(every dog).) presupposes nothing, so some = plain ∃ (also NIBLI_EXISTENTIAL_IMPORT=0)
:contradictions Scan the KB for contradictions
:trace <predicate> Enable tracing for a predicate
:untrace <predicate> Disable tracing for a predicate
:traces List all active traces

Transparency Triad UI

Nibli includes a standalone web UI (Dioxus) — the full reasoning engine (nibli-kr → nibli-semantics → nibli-reason) is compiled into the WASM bundle and runs entirely in the browser. nibli has no server.

# Start the web UI (port 8080)
just ui

To build a release bundle (just build-ui) or self-host, see DEPLOY.md.

The three tabs are Source (plain English), nibli KR (the formal encoding), and Back-translation (the structure-exposing gloss). The reasoning is fully local; the only optional network call is Formalize on the Source tab — a bring-your-own-key LLM request sent directly from your browser to a provider you choose (Anthropic, OpenAI, OpenRouter, Google Gemini, or any OpenAI-compatible/local endpoint). Configure it via the gear button: the API key is held in that tab's memory only — never persisted to storage and never routed through any nibli server (there is none), and it is erased on tab close/reload.

Formalize runs the agentic formalizer (nibli-formalize) — "formalize", not "compile": the LLM step is interpretive and sits outside the reasoning firewall, behind deterministic gates. The LLM's draft is validated by the real compilers — the nibli-kr front-end (grammar + fail-closed name resolution) + nibli-semantics (semantics) + a canonical render round-trip check — and any compiler error is fed back for the model to self-correct, so what lands in the nibli KR tab already passes those gates. It is still a draft — you review the nibli KR (and its back-translation) before the deterministic engine reasons over it, and you can skip Formalize entirely and type nibli KR directly.

The header has an example dropdown that loads a preloaded knowledge base into the triad — book case studies Syllogism (Ch 18), GDPR compliance (Ch 19), and Drug interactions (Ch 20), plus an optional extra playground corpus when shipped. In an example the KB source is read-only, Formalize is disabled, and the query box becomes a dropdown of that example's preset queries (selecting one runs it immediately). The default, Custom, is the editable mode. Book-facing corpora include the committed gdpr.nibli and drug-interactions.nibli files the engine's regression tests pin.

The UI uses a stateless KB model: every query builds a fresh engine, re-asserts the full KB tab as the knowledge base, then runs the query. The query bar is queries only (no assertions). The KB tab is the single source of truth.

As in the REPL, you state the claim to check, not ask a question: type eats(Adam). ("Adam eats"), not "Does Adam eat?". The query box shows a fixed ? purely as a reading cue — it is never typed into the field and never reaches the engine; the verdict (TRUE / FALSE / UNKNOWN) is the answer.

animal(every dog).            # Every dog is an animal
eats(every animal).           # Every animal eats
dog(Adam).                    # Adam is a dog

Query: eats(Adam).            # state the claim -> TRUE + proof tree

The interface is styled with the QUINE design system — an instrument-grade, terminal-first look (IBM Plex Mono, ember accent, blueprint-grid proof well) where every meaning-bearing color is a semantic token (verdicts, proof rule types, error classes) paired with a glyph for colorblind safety. Styling lives in nibli-ui/assets/tokens.css (design tokens) + nibli-ui/assets/style.css. Dark is the default; a header toggle switches to the light "paper" theme via data-theme="light".

Compute Backend

Nibli can dispatch predicates to external compute backends via a TCP + JSON Lines protocol. Any language that speaks TCP and JSON can serve as a backend.

# Terminal 1: Start the Python reference backend
just backend

# Terminal 2: Run Nibli with the backend connected
just run-with-backend

# In the REPL:
:compute exponential                # Register exponential for external dispatch
exponential(8, 2, 3).               # Assert: 8 = 2^3
? exponential(8, 2, 3).             # Query: TRUE (computed by Python)

Built-in arithmetic (always local, no backend needed): product (multiply), sum (add), quotient (divide).

One deliberate approximation. product/sum/quotient check x1 = x2 ∘ x3 with tolerant float equality — isclose with relative tolerance 1e-9 (matching Python's math.isclose), i.e. |a − b| ≤ 1e-9 · max(|a|, |b|). So 0.3 = 0.1 + 0.2 answers TRUE despite IEEE-754 rounding making the sum 0.30000000000000004. That is a real, bounded approximation on the numeric result — the one place Nibli is not bit-exact. The exact-equality predicate num_equal (=) is exact (==, tolerates no rounding); quotient's divide-by-zero check is likewise an exact guard. The single evaluator (nibli-types/src/arithmetic.rs) is shared by the in-WASM engine, the nibli-host host, and the Python reference backend, so all three agree.

Asserted numbers are quantifier-domain members. A number appearing in anything you assert — a fact or a rule's operands, mirroring how constants are noted — is enumerated like any entity: with big(5). asserted, sum(every big, 2, 3). is TRUE because 5 was checked (not vacuously), the arithmetically false sum(every big, 2, 2). is FALSE with 5 as its counterexample, and exactly N / no / some all agree with the universal. Two deliberate boundaries: a number a computed result auto-asserts mid-query does not join the domain (querying never grows the domain), and non-finite values (NaN/±inf — never spellable in nibli KR's digits-only numbers, but injectable via RDF import, :assert, or the WIT term API) are skipped fail-closed. See GUARANTEES §Disclosed Sharp Edges for the full contract.

External predicates (via backend): exponential, logarithm, and any custom predicates you add to the backend server.

Trust boundary. An external predicate is a trusted oracle, not something Nibli proves. When the backend replies true, that result is auto-asserted into the knowledge base as a ground fact mid-query, and the reasoner's rules chain on it exactly like a premise you asserted. Nibli never re-derives or checks it — the backend (and whoever operates it) is part of the trusted computing base. A proof that passes through exponential/logarithm is sound only relative to that oracle.

Computed facts are transient. The auto-assert above writes the typed fact store only — no fact id, no provenance record. A computed fact is therefore invisible to :facts, cannot be retracted by id, and is dropped by any rebuild (a retraction, a failed assertion's rollback, a trap replay). Built-in arithmetic shares this path: product/sum/quotient involve no oracle and no network, but a true result is auto-asserted exactly the same way. The lifecycle is an open decision, not a settled contract — see TODO.md §Compute / fact lifecycle.

Configure with NIBLI_COMPUTE_ADDR=host:port or :backend host:port in the REPL. Connection is lazy (connects on first dispatch) with auto-reconnect. The browser UI has no TCP, so external predicates resolve only in the nibli-host REPL; built-in arithmetic still works everywhere.

If an external predicate's backend is unreachable (or unconfigured), the query returns UNKNOWN (backend-unavailable) — never a definitive FALSE. A backend the engine cannot consult is genuinely undetermined, not a derived falsehood. One qualifier: an outage is not uniformly UNKNOWN. If that exact tuple was computed successfully earlier in the same session, its auto-asserted fact is still in the store and the query answers TRUE from it — outage-cache semantics, tracked alongside the lifecycle decision above. Any other tuple of the same relation still returns UNKNOWN.

Tech Stack

Component Technology
Language Rust (stable, 1.94.0)
WASM target WASI Preview 2 Component Model (cargo-component)
WASM runtime Wasmtime
Reasoning Demand-driven backward chaining over indexed fact store
Front-end parser pest (nibli KR — the grammar file is the parser)
Dictionary Compile-time perfect hash function (PHF)
Dev environment Nix flake
Compute protocol TCP + JSON Lines
Task runner Just
Web UI Dioxus (standalone — engine compiled into the WASM bundle)

Reasoning Engine

  • Backward chaining over a typed, hash-indexed fact store with predicate-indexed lookup
  • Universal rules compiled to backward-chaining templates (UniversalRuleRecord) at assertion time
  • Skolemization: independent constants and dependent Skolem functions (SkolemFn + DepPair for multi-dependency)
  • Proof traces: every query produces a proof tree (20 ProofRule variants) with DAG memoization via ProofRef
  • Witness extraction: query-find returns all satisfying binding sets for existential variables
  • Belief revision: retract-and-rebuild with monotonic fact IDs; :retract <id> and :facts REPL commands
  • Four-valued query result: TRUE, FALSE, UNKNOWN (cycle cut / incomplete knowledge / NAF dependent / backend unavailable / non-finite), RESOURCE_EXCEEDED (depth / fuel / memory)
  • Temporal reasoning: Past/Present/Future wrappers preserved end-to-end; timeless rules automatically derive tensed conclusions
  • Neo-Davidsonian event semantics: every predication decomposes into event type + role predicates; compound predicates share event variables
  • Conjunction introduction: And(A, B) verified recursively with mutual InDomain entities (bounded, no exponential blowup)
  • Numerical comparisons: greater (>), less (<), num_equal (==) evaluated at query time on Num terms
  • Compute dispatch: compute-backend WIT protocol with ComputeNode IR variant; results auto-asserted into KB
  • Ground conjunction flattening: top-level And trees flattened before assertion; ground material conditionals auto-registered as zero-variable rules for modus ponens
  • Equality reasoning: du (identity) with union-find congruence closure
  • Stratification enforcement: predicate dependency graph analysis prevents unsound negative cycles
  • Stratum-ordered materialisation: the stratification is also USED, not only checked — the relations a query reads under ~ are saturated bottom-up in stratum order, so ~p(x) is a set-membership test rather than an exhaustive attempt to prove p(x) and fail. Fail-closed: tense/deontic flavours, du equivalence classes, compute conditions and non-projectable rules are refused and keep the ordinary backward-chaining path. NIBLI_MATERIALIZE=0 turns it off
  • Integrity constraints: deny rules enforce assertion-time invariants
  • Defeasible rules: priority-ordered rule matching (priority: u32)
  • Sorted logic: type hierarchy with subsort checking
  • Hypothetical reasoning: with_assumptions() for clone-query-discard patterns
  • Selective forward chaining: forward: bool on rules with trigger_forward_rules
  • Aggregation: count_witnesses, aggregate(Sum/Min/Max/Avg)
  • Persistent fact store: FactStore trait with InMemory, Redb, and WASI backends
  • Iterative deepening: shallowest-proof guarantee
  • Tabling: cached results with invalidation on mutations
  • KB import/export: RDF Turtle parser, OWL class mapping via the nibli-import crate and CLI (just import <file.ttl>, with --raw/--export/--lang/--query flags)
  • Failure traces: PredicateNotFound, RuleAttemptFailed, EqualitySubstitution proof rule variants explain why derivations fail
  • Argument-position indexing: (relation, position, value) secondary index for efficient witness extraction
  • Predicate signature validation: arity checking from PHF dictionary with permissive warnings
  • Closed-world visibility: naf_dependent (a na→True NAF result) and its dual cwa_false (a FALSE that is closed-world — "not derivable", not a disproof — vs. a numeric FALSE that was decided) flag CWA-dependent conclusions on every proof trace; both render a closed-world caveat
  • Interactive debugging: :trace/:untrace/:traces REPL commands
  • WASM fuel limits: configurable via NIBLI_FUEL or :fuel REPL command
  • WASM memory limits: configurable via NIBLI_MEMORY_MB or :memory REPL command
  • Error types: nibli-error variant (syntax/semantic/reasoning/backend) with line:column for parse errors
  • Batch loading: :load <filepath> loads .nibli files; # lines are comments

Development

Command Description
just run Full pipeline: build WASM component, launch REPL
just check Fast type-check (cargo check --workspace)
just test Run all unit tests
just test-engine Integration tests (full parse → compile → reason pipeline)
just test-nibli-kr nibli KR front-end tests only
just test-backend Python backend tests
just test-all Every test suite
just verify-nibli-kr-seam The KR seam gate (FOL structural goldens + construct sweep + metamorphics)
just ui Standalone Transparency Triad web UI (port 8080)
just backend Python reference compute backend (port 5555)
just run-with-backend Build + run with compute backend
just run-persist Run with persistent Redb fact store
just fuzz-nibli-kr [SECS] Fuzz the nibli KR front-end
just fuzz-assert [SECS] Fuzz assertion pipeline
just fuzz-query [SECS] Fuzz stateful KB queries
just fuzz-ci [SECS] Time-boxed fuzz gate (all 3 targets, corpus-seeded) — runs in CI
just ci Full CI suite
just clean cargo clean

License

See LICENSE for details.