munu
Munu is the first language designed with the LLMs as first-class readers. Errors are structured for machines. Contracts are the harness that holds AI agents to their obligations — proven at build time, observed at runtime.
The language LLMs can actually drive.
Every property models need — structure, proof, supervision — promoted from convention to construct. The kernel only steps bytecode; the rest lives in source the model can read.
Formal Verification
Contracts carry requires, ensures, and decreases clauses. The compiler proves them at build time — no runtime checks, no test suites hoping for coverage.
LLM-First Diagnostics
Every error is a JSON envelope: failing constraint, AST positions, candidate-fix vector, smallest counter-example. The compiler is the first reader; the LLMs are the second; the human, when they choose to look, is the third.
Agent Harness, Not Library
Supervision trees are first-class. do: handles local failure; must: enforces obligations to the parent. Model tool-use becomes a contract — and the contract is the substrate the kernel runs.
Errors written for the machine.
Every other compiler emits prose. Munu emits a JSON envelope with the failing constraint, the AST positions, a candidate-fix vector, and the smallest counter-example. LLMs patch; humans review the diff.
error[E0308]: mismatched types --> src/main.uv:14:18 | 14 | let n: u64 = raw | ^^^ expected u64, found ψ | = help: add a cast # LLMs must parse English, guess intent, # infer the patch from sparse context.
{ "code": "M.subsume.fail", "operator": "⊑", "expected": "u64", "got": "ψ", "site": "src/main.uv:14:18..14:21", "ast_node": "@blake2b:f12a…", "constraint": "ψ ⊑ u64", "witness": { "raw": "-3.14" }, "fixes": [ { "k": "insert_cast", "term": "raw as u64" }, { "k": "widen_target", "term": "i64" } ] }
Contracts, not functions.
A contract witnesses the agreement between an algebra (μ — what you build) and a coalgebra (ν — what you observe). The do: clause governs local failure recovery. The must: clause is the obligation to the supervisor.
For LLMs driving agent loops, this is the harness: every tool-use, every retry, every escalation is a contract the kernel can prove and the runtime can observe. Breach is permanent — no retry, no catch.
Deep dive into the methodology// A supervised gate contract contract Gate(input: Stream<Frame>) { do: permanent() must: responds_within(100ms) mu validate(frame: Frame) -> Result { requires frame.len <= 1024 ensures (r) r.is_ok() => frame.checksum_valid() decreases frame.ttl ... } nu forward(validated: Stream<Frame>) { // coinductive: observe forever route(validated.head) |> emit forward(validated.tail) } }
Where LLMs meet the real world.
LLM Agent Harness
Contracts as guardrails for tool-use, retries, escalation
Embedded Systems
Verified firmware on Cortex-M0 & RISC-V
Distributed Networks
BlackFrame protocol for trustless coordination
Edge & Codegen
WASM contracts in browsers and CDN workers