The first tagged release of nibli — a zero-hallucination symbolic reasoning engine: a deterministic theorem prover compiled to WebAssembly (WASI P2), with the nibli KR predicate-call language as its front-end.
0.x caveat: minor versions may break APIs; the embed surface (nibli-engine) is not yet declared stable. See CHANGELOG.md for the full notes and GUARANTEES.md for what the engine does and does not promise.
Highlights
- The pipeline: nibli KR (
nibli-kr) → First-Order Logic IR (nibli-semantics, spec inLOGIC_IR.md) → demand-driven backward chaining (nibli-reason), shared by every surface throughnibli-session::CoreSession. - Runtime surfaces: the
nibli-pipelineWASM component (nibli:engine@0.7.0WIT) under thenibli-hostWasmtime REPL; the nativenibli-engineembedding; the in-browser playground. - Guarantees and gates: differential soundness against Vampire and clingo, six mechanized Lean 4 proofs with Rust conformance bridges, KB-level behavioural pins, fuzzing, mutation-testing baseline.
- The committed English corpus: the dictionary is validated Rust source — no network at build time.
Assets
| File | What |
|---|---|
nibli-pipeline-v0.1.0.wasm |
The WASM component (wasm32-wasip2, release) — run under nibli-host via NIBLI_WASM_PATH |
nibli-host-v0.1.0-x86_64-linux |
The Wasmtime host + REPL (Linux x86-64) |
nibli-validate-v0.1.0-x86_64-linux |
The validation CLI (Linux x86-64) |
SHA256SUMS |
Checksums for the above |
Docs: https://dhilipsiva.github.io/nibli/ · Playground: https://dhilipsiva.dev/nibli-playground/