Muro.

The thesis.

Muro’s author describes it as agent-centric. The agent absorbs the cognitive load of formal verification, and people get verified programs that run on an established runtime. The language is built to make that division of labour checkable. Nothing is inferred: there are no implicits, unification, metavariables or tactics, so every type, motive and proof step an agent produces is on the page. mix muro.check either accepts the file or names each definition that fails.

A spec never becomes evidence. Evidence never becomes a run.

Muro (Spanish for wall) is an explicit affine dependent type theory implemented in Elixir, with the rules of the calculus written in Agda under agda/Muro/. Every definition is tagged spec, evidence or run. spec definitions describe data and signatures and are never compiled. evidence definitions are theorems written as ordinary terms (match, rewrite, refl), checked to the same standard as programs and then erased. run definitions are programs: affine in their variables unless plain data is marked reusable, and structurally recursive on one argument. From one source, run terms emit as Elixir def/defp for the BEAM or, with mix muro.emit --backend c, as a .h/.c pair. The author has said more targets are planned; none beyond these two exist yet.

What it looks like.

def IsEven : spec Π (n : Nat) → Type := …
def half : run Π (n : Nat) → Nat := …
def half_ok : evidence Π (n : Nat) → Π (e : IsEven n) →
    {plus (half n) (half n) ≡ n : Nat} := …

Distinctive moves.

• The wall. The site’s mode table: a run term may appear in run, evidence and spec; an evidence term in evidence and spec but never in run; a spec term only in spec. A proof may talk about a program; a program may not depend on a proof. Passing a value to a theorem does not spend it.
• Nothing inferred. No implicits, unification, metavariables or tactics. A ? hole always fails and reports the expected type and context.
• Checker soundness in Agda. Muro.Soundness proves, under --safe, that when the Elixir-mirrored checker accepts a definition, the inductive judgment derives it — one direction only, on a fragment covering Π, λ, Nat, Unit, Empty, identity, rewrite and indexed data/match. Streams (ν) and Tensor sit outside that proof, and the project states that consistency for closed evidence waits on normalisation.
• Fuel is not a verdict. Reduction is bounded by fuel; running out is reported as out of fuel, not as acceptance.

Maturity.

First commit 18 September 2026; published on Hex by the murolang organisation, with a per-release changelog. The C backend (Muro.Emit.C) landed on 1 October 2026 and is narrower than the Elixir one. It handles Nat, Unit, user and indexed data, match as switch, and run streams as seed-plus-step structs. It refuses I64/F32/Tensor (c:machine), closures and unapplied lambdas (c:lambda), and Always, ~ or raw ν inside a run (c:stream). Allocation goes through an overridable MURO_ALLOC. CI runs the Elixir tests, including C tests that compile the output with cc, and make agda on every push. Examples include Vec/Fin lookup without runtime bounds checks, streams with bisimulation, Nx-backed machine numbers, and a reinforcement-learning library (CSHRL) whose environments prove ranking theorems and emit an agent as an Elixir Stream. The manual’s Limits page lists what the checker refuses.

Agent tooling.

The README states that Muro is built for agents to write, with the agent carrying the load of formal verification. A root AGENTS.md condenses the manual’s For agents page. It separates two jobs (writing a .muro program versus changing the kernel), lists allowed and forbidden edits and the exact commands (including --fuel and emit for both backends), and instructs agents to “copy syntax from examples/, not from memory”. It also records practical pitfalls: parenthesising a multi-line match used as an argument, an affine reuse being reported as non-descending recursion, branch order following constructor order, erased guards not ruling out run branches, and slow unary Nat constants. The repository ships an llms.txt index of the manual, and manual/manifest.yml is a machine-readable index of the same pages. Diagnostics are plain text with line:col positions, and holes print the expected type and context. There is no SKILL.md, MCP server or JSON diagnostic output.