nibli-formalize

The agentic English→KB formalizer engine for the Transparency Triad (fanva = Lojban "translate" — the crate name predates THE FLIP). An LLM formalizes English into the KB language (nibli KR by default; legacy Lojban behind the same Language seam); the real nibli compilers verify; errors are fed back until the KB text is valid. Surfaced inside nibli-ui as the Formalize mode (this crate holds no UI). "Formalize", never "compile": the LLM step is interpretive and sits outside the reasoning firewall, behind the deterministic gates below.

The loop

An LLM drafts KB text — in legacy Lojban mode it may call jbotci's dictionary/grammar tools while drafting — and every candidate must then clear a three-gate, fail-fast, local firewall before it is accepted:

• nibli KR (default): nibli_kr::parse_checked (grammar + fail-closed name resolution) → nibli-semantics (semantics/arity) → the render round-trip gate (the candidate's canonical nibli_kr::render re-spelling must re-compile to the SAME LogicBuffer — nibli-kr's fixpoint contract as a per-candidate drift-catcher; pure Rust, runs native + wasm).
• Lojban (legacy): nibli-kr::parse_checked → nibli-semantics → the official camxes parser (wasm-only JS-interop; skipped on native / without the shim).

A rejection feeds the compiler's own message back (gates::feedback_for) and the LLM retries, bounded by max_attempts with an oscillation guard. A gate-clean candidate then faces the semantic verification turn (verify.rs): a fresh-context judge reads the engine's own IR-level back-translation of each KB line and a MISMATCH retries through the same loop — best-effort advisory, fail-open. This is the formalization step (agent::translate_agentic): it runs before the KB text is shown, and is separate from the engine's own front-end→nibli-semantics→nibli-reason compile that nibli-ui runs later, at query time.

flowchart TD
    src(["English source"]) --> disc{"legacy Lojban mode with<br/>jbotci enabled + proxy reachable?"}
    disc -->|"no / unreachable / nibli KR mode"| deg["no tools · run degraded<br/>(local gates only)"]
    disc -->|yes| have["discover jbotci tools once<br/>dictionary · grammar · morphology"]
    deg --> loop
    have --> loop

    loop{"attempt n ≤ max_attempts?"} -->|"no · cap reached"| exh["Exhausted<br/>best effort + last error"]
    loop -->|yes| gen

    subgraph turn["LLM turn — run_llm_tool_loop, up to max_tool_steps"]
      direction TB
      gen["LLM proposes candidate KB text"] --> tcq{"model called<br/>a jbotci tool?"}
      tcq -->|"yes · optional tool-use (Lojban mode)"| mcp["MCP call via the proxy<br/>vlacku · cukta · gentufa · vlasei · …<br/>result fed back to the model"]
      mcp --> gen
    end

    tcq -->|no| clean["clean_lojban_output → candidate"]

    clean -->|"per non-comment KB line"| g1{"gate 1 · front-end<br/>nibli-kr (default) / nibli-kr (legacy)<br/>parse_checked — grammar"}
    g1 -->|ok| g2{"gate 2 · nibli-semantics<br/>compile_from_ast — semantics / arity"}
    g2 -->|ok| g3{"gate 3 · per language<br/>nibli KR: render round-trip (native+wasm)<br/>Lojban: camxes official_gate (wasm-only)"}
    g3 -->|ok| ver{"semantic verification turn<br/>fresh-context judge reads the<br/>IR back-translation (advisory)"}
    ver -->|MATCH / fail-open| ok["Success<br/>validated KB text → KB tab<br/>(nibli-ui compiles the FOL later)"]

    g1 -->|reject| osc
    g2 -->|reject| osc
    g3 -->|reject| osc
    ver -->|MISMATCH| osc

    osc{"candidate same<br/>as previous attempt?"} -->|"yes · oscillation"| exh
    osc -->|"no · append feedback_for"| loop

    gen -.->|"provider / network / auth error"| cf["ChatFailed<br/>transport error, not an invalid KB"]

    classDef good fill:#1a7f37,stroke:#116329,color:#fff;
    classDef warn fill:#9a6700,stroke:#7d4e00,color:#fff;
    classDef bad fill:#cf222e,stroke:#a40e26,color:#fff;
    class ok good;
    class exh warn;
    class cf bad;

Gates 1–3 are gates::local_gates + gates::validate, all keyed on nibli_types::lang::Language. jbotci (vlacku/cukta/tersmu/gentufa) is Lojban-only tooling, optional even there — reached only through an app-owned proxy — and used as LLM tools + the tersmu meaning view, never as a required gate. No proxy (or nibli KR mode) ⇒ local gates only, fully serverless.

Test discipline

• Local gates (both languages, incl. the round-trip gate) + provider/agent logic + the verification turn: native cargo test -p nibli-formalize --lib (just test-formalize) with mocked chat() / MCP; the two shipped system prompts are pinned by gate-validity guard tests over their few-shots.
• MCP client (gloo-net) + the camxes official_gate (JS-interop): wasm-only, covered by wasm-pack test (just test-formalize-wasm).