The live demo below runs nibli — a symbolic-reasoning engine (Rust→WebAssembly) that derives every answer with a proof trace, entirely in your browser — and needs JavaScript + WebAssembly. More on the engine in things I built and musings.

// nibli · live demo

The hallucination firewall, running in your tab

This is the real engine — nibli-kr (parser), nibli-semantics (semantic compiler), and nibli-reason (backward-chaining reasoner) — compiled from Rust to WebAssembly. Nothing is mocked and nothing leaves your browser: every query below runs live deduction over the loaded knowledge base, and every answer carries its proof.

TRUE FALSE UNKNOWN RESOURCE_EXCEEDED — every query returns exactly one of these. There is no confident-sounding middle ground. The engine never guesses.

Open the full playground → This page is a guided tour. The playground is the complete app — write your own nibli KR, formalize English with your own LLM key, and inspect every proof.

engine: loading wasm…

1 · Source // what a human wrote 2 · Formal encoding // nibli KR, asserted live 3 · Back-translation // the logic, read back in English

structure-exposing English rendered from the compiled first-order logic (nibli-render) — the verification surface, not prose

// ask the engine

// change the world, watch the proofs follow

// why three panes — how the triad catches an LLM

In the full pipeline an LLM drafts the nibli KR from English — and LLMs make fluent mistakes. The deterministic back-translation is what catches them. A worked example from the book (Ch 20): the source says “Every person who has not consented must have their data erased.”

LLM draft obligated(some person where ~approves, event { removes() }). → “some person who has not consented must be erased …” REJECTED “some” ≠ “every” — a quantifier the eye catches instantly in the gloss

Corrected obligated(every person where ~approves, event { removes() }). → “every person who has not consented must be erased …” ACCEPTED the human verifies the gloss, never the model's confidence

// the honest part

Soundness is about inference, not premise truth. Like Lean or Coq: if the engine says TRUE, a formal derivation exists from the asserted axioms — but garbage premises still yield garbage conclusions, validly derived. And under the closed-world assumption, FALSE means “not derivable from the current knowledge base” — not “known false in the real world.” The proof trees flag every step that leans on that assumption. Read more in the book or the source — or ask my twin about it, which is itself the problem nibli exists to solve.