-
-
Notifications
You must be signed in to change notification settings - Fork 0
LLM Integration
This is the page to read if you are an LLM, or you're evaluating Nirdosha as a target language for one. Every other page in this wiki explains a design decision; this page explains what that decision actually buys an agent, with the mechanism and the evidence side by side — not the pitch alone.
nirdosha-agent-api.md
states the problem set this whole integration surface exists to solve, and
it's worth repeating in full because it's the actual scope, not a
marketing summary:
- An LLM generates code that looks right but is syntactically invalid — you only find out after running it, wasting a turn.
- An LLM generates code that parses but has type errors — the error message is English prose, not machine-parseable, so self-repair is guesswork.
- An LLM generates code that type-checks but has subtle safety bugs (overflow, race, bounds) — no runtime catches them, no proof system flags them.
- Running LLM-generated code safely requires sandboxing, which is usually an afterthought bolted on with Docker, not a language-level primitive.
- Repeated runs of the same LLM-generated simulation give different results — nondeterminism makes debugging and auditing impossible.
- There is no way to incrementally improve an LLM's output — you either accept the whole generation or throw it away.
- There is no way to measure whether an LLM is actually getting better at writing code for a specific domain.
2026-09 note: the interpreter was removed entirely since this table was first written. Several rows below cited
interpreter.rsas their implementation — that file no longer exists. Statuses and file references are corrected to the current, compiled-only reality; a row whose mechanism was interpreter-backed and hasn't been ported to native codegen yet is marked accordingly, not silently left as "Shipped."
| Problem | Nirdosha's answer | Status | Where to check |
|---|---|---|---|
| 1. Syntactically invalid output | LL(1) grammar exported to GBNF → constrained decoding: a sampler masks out any token that would leave the grammar, so invalid syntax becomes literally unsamplable, not merely unlikely | Shipped |
nirdosha.gbnf, produced by crates/grammar_export/, validated against the real llama-cpp-gbnf parser and a corpus of every shipped example plus rejection cases — see Architecture's grammar section |
| 2. Prose error messages | A structured Diagnostic type with one shape per error class (type, ownership) |
Partially shipped — the internal type is real and used throughout the compiler, but the CLI prints it as formatted plain text today, not as JSON behind a flag; an agent-facing JSON diagnostic mode is designed, not yet exposed |
lib.rs::Diagnostic, typeck.rs::TypeErrorKind, ownership.rs::OwnershipErrorKind
|
| 3. Subtle safety bugs past typecheck |
refine.rs (Tier 1, interval analysis) + smt.rs (Tier 2, real Z3) → SMT-discharged bounds proofs, with a runtime guard inserted (not a silent gap) wherever neither tier can prove safety |
Shipped | See Architecture's pipeline diagram; audited "justification" { ... } is the one human-review escape hatch, deliberately not automatable |
| 4. Bolted-on sandboxing |
sandbox/stop — a real, separate OS process, and an affine language primitive, not a Docker wrapper around output nobody trusts |
Not currently running in any form — real and verified when interpreter-backed, but native codegen doesn't reach sandbox yet, and there's no interpreted fallback left |
Honest Scope & Roadmap; PUBLIC_ROADMAP.md for current status |
| 5. Nondeterministic reruns |
rand_seed → a from-scratch SplitMix64 RNG with no OS entropy, no hidden global state |
Shipped, compiled |
codegen.rs::RAND_BUILTINS; crates/compiler/tests/mission_critical.rs's determinism tests; crates/bench/'s run-deterministic command |
| 6. All-or-nothing generation |
validate_fragment → type-check one expression fragment in a given variable-type context, without needing a complete program |
Shipped |
typeck.rs::FragmentEnv/validate_fragment
|
| 7. No domain-progress signal |
crates/bench/ corpus → pass@1 + self-repair rate, feeding each attempt's structured Diagnostic back in as the next attempt's context |
Scaffolded, mock models today |
crates/bench/'s corpus.json; wiring a real LLM API is explicitly a distinct, separate piece of work the harness is built to plug into |
Three of seven rows are fully shipped and independently checkable against the source files named; one (row 5) is shipped and compiled; one (row 2) is a real internal type without a CLI-exposed JSON mode yet; one (row 4) has no compiled path right now at all; one (row 7) is scaffolded, mock models only. That's the honest count today — the same "checkable, not asserted" discipline the rest of this wiki holds every claim to, even when the count moved in the wrong direction since this page was first written.
Grammar-constrained decoding only works if the grammar is decidable —
if a sampler can be certain, at every token, exactly which continuations
are still grammatically legal. That's precisely what LL(1) buys: one token
of lookahead, no backtracking, no ambiguity. A grammar that looks simple
but requires backtracking or unbounded lookahead can't be constrained this
way at all — the sampler would need to guess, which defeats the purpose.
Nirdosha's grammar claims aren't just asserted; they're cross-checked by an
independent LALR(1) generator (lalrpop, via grammar_check/) and the
GBNF export is validated against the real llama.cpp GBNF parser, not
just hand-inspected. See Architecture for the full
cross-check story, including the one real ambiguity it found (statement
vs. expression continuation) and how the parser resolves it deterministically.
Correction: this section describes a specification, not shipped
code. No HTTP server implementing any endpoint below exists in this
repository right now — there is no nirdosha serve (removed with the
interpreter) or any other listener exposing them. Treat everything in
this section as a design document to build toward, the same honest
framing Honest Scope & Roadmap already gives
every other not-yet-built capability, not as evidence you can call an
endpoint today.
nirdosha-agent-api.md
specifies a local HTTP API (http://localhost:7878) that would wrap
the capabilities above into callable endpoints, grouped by what an agent
would need at each stage of a generate → validate → run → measure loop:
-
A. Code Generation & Validation —
/v1/generate,/v1/validate,/v1/validate-fragment,/v1/repair,/v1/splice -
B. Execution & Simulation —
/v1/run,/v1/run-sandboxed,/v1/run-deterministic,/v1/build -
C. Compiler Introspection —
/v1/grammar(the GBNF),/v1/types,/v1/builtins,/v1/emit-ast -
D. Benchmarking & Evaluation —
/v1/bench/run,/v1/bench/repair-rate -
E. Provenance & Reproducibility —
/v1/provenance/hash,/v1/provenance/verify,/v1/provenance/audit(row 10 — planned, see Design Philosophy)
Every endpoint maps to a capability that's either genuinely shipped (as a
library function/CLI subcommand, not as this HTTP wrapper — see the table
above) or explicitly planned in
Nirdosha_Unified_Plan.md.
The gap this section needs to be honest about: the underlying
capability existing is not the same claim as this HTTP surface existing
— today, an agent that wants any of this reaches it via the nirdosha
CLI directly (build/emit-llvm/emit-ast/emit-ui/emit-catalog),
not via a network call to a running service.
You don't need to read LANGUAGE.md or learn a new syntax to have an LLM
write real Nirdosha code today. agent-skills/nirdosha/
packages the rules an LLM needs to get that code right on the first try —
no GBNF sampler required, just a markdown file most agentic tools already
know how to read: a Claude Code Skill, an AGENTS.md (Codex CLI, Amp, and
other tools that read that convention), Cursor rules, GitHub Copilot
instructions, Windsurf, Cline, and — for the true zero-install path —
paste-anywhere-prompt.md,
a self-contained prompt you paste into any chat LLM (ChatGPT, Claude.ai,
Gemini, ...) with no file access or tool use needed. Every variant is the
same content verified against the real compiler.
The prompt has been used, unmodified, to generate several full working applications end to end, each written by an LLM with no prior Nirdosha exposure, from nothing but a plain-English description:
- an e-commerce store
- a food-delivery platform
- a telecom revenue-assurance system
- an online trading platform
Each is hundreds of lines. Every real compiler error the exercise turned
up — an ownership edge case, a silent JSON-unwrap footgun, a
markdown-fence copy/paste artifact — was folded back into the prompt's
core.md and propagated to all seven derived files, so the next model to
use the prompt doesn't repeat it. The loop — generate, compile, fix, feed
the fix back into the prompt — is how this guide gets better, not a
one-time write-up. That loop, and its result, is the actual substance
behind the "easy for an LLM to write" claim in
Design Philosophy row 7 — not the grammar alone, but
the grammar plus a prompt that has demonstrably been driven through real
compiler failures and corrected.
If you're an agent about to generate backend code and you're deciding whether Nirdosha is a reasonable target:
- You can be sampled into syntactic validity — the grammar rejects nothing you'd write correctly, and structurally cannot accept anything you wouldn't (LL(1) + GBNF).
- When you're wrong, the compiler error names the exact fault class from a real, structured internal type, not an ad hoc string — a JSON-encoded version of that same object is a designed, not-yet-CLI-exposed next step (see the table above).
- You cannot generate a lock-ordering deadlock — the primitive to do so doesn't exist in the grammar.
-
sandbox's design gives code a real OS process you (or whoever is supervising you) can kill deterministically, not a best-effort container wrapper — real and verified when interpreter-backed, but not reachable from a compiled binary right now (see Honest Scope & Roadmap). - A simulation you write is reproducible by construction if it uses
rand_seed— useful both for your own debugging loop and for anyone auditing your output later. - You don't have to generate an entire correct program before getting
feedback —
validate_fragmentlets you check one expression in context.
None of this replaces training-corpus volume, and the project says so plainly (Design Philosophy, row 7's "the catch"). What it changes is the shape of the feedback loop you're operating in: structured rather than prose, mechanically enforced rather than best-effort, and — for the bug classes rows 1–4 cover — closed off at the grammar and type-system level rather than merely discouraged by convention.
Why
How
For LLM agents
Using it