Build. Prove. Observe.

munu

A distributed programming language and harness built for LLMs to read, write, and prove correct. Build with mu functions. Prove with contracts. Observe with nu streams. The kernel runs everywhere — MCU to cloud.

Why Munu

LLMs have blind spots. Munu closes them.

Every weakness that makes LLM-generated code dangerous has a language-level mitigation. Not a linter. Not a convention. A construct the compiler enforces.

Hallucination

requires/ensures prove correctness at compile time. The LLM can hallucinate — the contract won't verify.

Mutation tracking

Variables bind once. No reassignment, no temporal state, nothing for the LLM to simulate step-by-step.

Concurrency

Dataflow variables have a 6-state lifecycle enforced by the kernel. Reads block until bound. There is no race to reason about.

Ambiguous errors

The diagnostic is a structured envelope: failing constraint, AST position, counter-example, candidate fixes. The LLM applies the fix — it doesn't interpret prose.

A taste of Munu

What it looks like.

A mu function builds a finite value. A nu function observes an infinite stream. A contract supervises both — if it crashes, the behaviour clause decides what happens next.

Deep dive into the methodology
echo.uv
// mu: finite, builds a value
mu double(n: i64) -> i64 {
  n => n * 2
}

// nu: infinite, observes a stream
nu echo_loop(msg: Msg) -> [Msg] {
  msg => [msg | echo_loop(msg)]
}

// contract: supervises both
pub contract Echo(msg: Msg) -> [Msg]
    behaviour { do: nu X. [_] X } {
  spawn echo_loop(msg)
}
Built For

Where contracts meet the real world.

LLM Agent Harness

Contracts as guardrails for tool-use, retries, escalation

Embedded Systems

no_std kernel — no heap, no OS, bare metal

Distributed Deployment

Ed25519 signed bytecode over BlackFrame

Edge & IoT

no_std kernel on MCUs, in WASM, and on servers