APPLICATIONS

Where formal meets practical.

Munu is designed for systems where correctness is not optional — AI agents that must obey constraints, firmware that must not crash, networks that must converge, and edge functions that must respond in time.

AI Agent Supervision

Contracts as guardrails for LLMs at tool-use time

When an LLM calls a tool, that call is a contract — every LLM in your stack reads the same constraint. The must: formula defines what the agent is allowed to do. The do: formula defines how it recovers from failure. Breach is not an exception — it's a permanent signal to the supervisor that the agent violated its obligation.

Why Munu
  • Formal bounds on agent behaviour — not just prompt engineering
  • Supervision trees that escalate, restart, or terminate agents
  • Structured diagnostics that LLMs can parse and self-correct from
  • Compose agent capabilities via lattice subsumption (⊑)
agent.uv 
nu serve(requests: Stream<Query>, tools: ToolSet) -> Result {
    requests, tools => {
        tools.call(requests.head)
    }
}

pub contract Agent(tools: ToolSet) -> [Result]
    behaviour {
        // two strikes: restart once, then escalate
        do:
            nu X. [fail(self, _)] <restart(self)>
            nu Y. [fail(self, _)] false
                 and [_] Y and [_] X
        must: true
    }
{ serve(requests, tools) }

Embedded Systems

Verified firmware on Cortex-M0 and RISC-V

Munu's kernel runs without an OS, without a heap, without a garbage collector. Contracts compile to bare-metal bytecode with static memory allocation. The requires/ensures/decreases clauses prove termination and correctness at compile time — critical for safety-rated firmware.

Why Munu
  • No runtime overhead — arena allocation, no GC pauses
  • Compile-time verification of timing and memory bounds
  • Same language for application logic and hardware drivers
  • Supervision trees replace ad-hoc watchdog timers
sensor.uv · target=cortex-m0 
extern mu sensor_read(channel: u64) -> u64;

mu read_temperature(channel: u64) -> i64
  requires channel > 0
  ensures  (t) t >= -40 && t <= 125
{
  channel => sensor_read(channel)
}

pub contract SensorDriver(channel: u64) -> [u64]
    behaviour {
        do:
            nu X.
                [from(self)]
                    <to(self)> true
                and [fail(self, _)]
                    <restart(self)> true
                and [_] X
        must: true
    }
{ sensor_loop(channel) }

Distributed Deployment

Ed25519 signed bytecode cascading across nodes

Node A deploys bytecode to node B; B deploys further down to C. Every hop verifies the Ed25519 signature chain. The wire format is BlackFrame — fixed 1024-byte, two-layer encrypted frames (ChaCha20-Poly1305 hop layer, X25519 forward secrecy on the E2E layer). Routing decisions are made by Munu contracts using greedy forwarding on the Poincaré disk; the kernel never touches the routing logic.

Why Munu
  • Fixed 1024-byte frames with two-layer encryption (hop + E2E)
  • Ed25519 signature chain verifies every deployment hop
  • X25519 ephemeral key per message — forward secrecy by default
  • Single-assignment dataflow — no conflicts, no CRDTs needed
deployment · A → B → C 
// Wire format per hop:
//   module_hash (32 bytes)
//   name_len   (1 byte)
//   name       (UTF-8, up to 255 bytes)
//   signature  (64 bytes, Ed25519)

// BlackFrame: 1024 bytes total
//   hop_nonce (12) + hop_ct (1012)
//     → ChaCha20-Poly1305 over HopPlaintext
//       version (1) + ttl (1)
//       + coord_hint (8, blake2b of angle)
//       + inner_ephemeral (32, X25519)
//       + inner_nonce (12)
//       + inner_ct (942)
//         → ChaCha20-Poly1305 E2E
//           payload (885 bytes)

Edge & IoT

The no_std kernel runs on MCUs, in WASM, and on servers

IoT devices run untrusted code on untrusted networks. Munu solves both problems at once: the no_std kernel runs verified contracts on bare-metal MCUs, and every byte on the wire is inside a BlackFrame — two-layer encrypted, Ed25519 signed, fixed-size. There is no "configure TLS" step, no certificate authority, no handshake protocol to get wrong. A sensor node and a server run the same kernel, the same bytecode, and the same cryptographic guarantees. Trusted computing from the MCU to the cloud.

Why Munu
  • Security built into the wire — BlackFrame encryption on every hop
  • Same verified bytecode on Cortex-M0, in WASM, and on a server
  • No TLS, no certificates, no handshake — Ed25519 identity from the seed
  • Kernel is no_std — no heap, no OS, cooperative scheduling
sensor_pair.uv 
// Same contract runs on MCU, WASM, and server.
// Only the extern changes per platform.
extern mu sensor_read(channel: u64) -> u64;

nu sensor_loop(channel: u64) -> u64 {
    channel => sensor_read(channel)
}

pub contract SensorPair(channel: u64) -> [u64]
    behaviour {
        do:
            nu X.
                [from(self)]
                    <to(self)> true
                and [fail(self, _)]
                    <restart(self)> true
                and [_] X
        must: true
    }
{ sensor_loop(channel) }

Formal Verification

Prove properties at compile time, not test time

Every mu function carries requires/ensures/decreases annotations. The compiler verifies termination, pre-conditions, and post-conditions statically. No separate proof assistant needed — verification is part of the language, not bolted on.

Why Munu
  • Termination proofs via decreases measures
  • Pre/post conditions checked at compile time
  • Lattice-based type inference catches contradictions early
  • No separate proof language — verification in the source
search.uv 
mu count_periods(n: u64) -> u64
  requires n > 0 && n < 1000
  ensures  (r) r >= 1 && r <= n
  decreases n
{
  1 => 1
  n => 1 + count_periods(n - 1)
}

mu calculate_interest(principal: i64, rate: i64, periods: i64) -> i64
  requires principal > 99 && rate > 0 && periods > 0
  ensures  (r) r > 0
{
  principal, rate, periods =>
    principal * rate * periods / 100
}

Ready to build?

Start with the compiler, write your first contract, and deploy to any target.

Get Started