// nibli · live demo

The hallucination firewall, running in your tab

This is the real engine — gerna (parser), smuni (semantic compiler), and logji (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.

engine: loading wasm…

1 · Source // what a human wrote

2 · Formal encoding // Lojban, asserted live

3 · Back-translation // robotic by design

word-by-word gloss from 10,521 jbovlaste entries — 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 Lojban from English — and LLMs make fluent mistakes. The deterministic back-translation is what catches them. A worked example from the book: the source says “Every employee must file an annual report.”

LLM draft su'o lo se ciska cu bilga … → “some the (swap-2) write must …” REJECTED “some” ≠ “every” — a quantifier the eye catches instantly in the gloss

Corrected ro lo se ciska cu bilga … → “all the (swap-2) write must …” 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.