marv

A compiled programming language whose author is a coding agent and whose auditor is a human.

Quickstart · Toolchain · For agents · Docs · Spec

marv (short for Marvin) takes one premise seriously: most code will be written by machines and read by people. Every design rule serves explicitness, local reasoning, and machine-verifiability — so a human auditor can trust agent-generated code by reading signatures, and an agent can generate→check→repair in a tight loop against a real compiler service.

What that means concretely:

• No hidden control flow or growable allocation. Every effect is visible at the call site; user-visible growable heap allocation happens only through an explicit Alloc capability.
• No ambient authority. There is no global I/O, clock, randomness, or network. Power enters a function only through capability parameters, recorded in its effect row — so a signature bounds everything a function can do. This is also the WASM sandbox model.
• Errors are values with inferred sets. The complete failure surface is recoverable from the type.
• Memory safety with no GC and no lifetimes — mutable value semantics + second-class references + linear resource types.
• Contracts are first-class — requires/ensures/invariant, runtime-checked in debug and SMT-discharged for a verified subset.
• The unit of identity is the content hash of a definition's Core IR. Renames are free, identical code dedups, and builds are reproducible by lockfile.
• The compiler is a service first, a CLI second — a salsa-backed incremental query engine behind a JSON-RPC protocol, built for the agent loop.

Status: the Stage-0 compiler (in Rust) is implemented end to end through milestones M0–M7 — front end, Core IR + content hashing, the type/effect/capability checker, the incremental query server, two execution backends (a tree-walking interpreter and a Cranelift JIT/AOT plus a first LLVM release slice), a WebAssembly backend with a capability-gated browser sandbox, layered verification (runtime contracts + SMT), and a content-addressed store with commit. Stage-1 self-hosting has a first tiny compiler-driver milestone in selfhost/driver.mv, with Rust Stage 0 still acting as compiler, oracle, and fallback for unsupported language surface. The language surface is still a growing subset (see Status & roadmap).

Prerequisites: a Rust toolchain (pinned to 1.94.0 via rust-toolchain.toml). For the Tier-2 SMT verifier, a z3 binary on PATH (brew install z3 / apt-get install z3); without it, verify honestly falls back to runtime checks.

For application projects, prefer a release toolchain: download the GitHub Release tarball for your platform, unpack it, and put the unpacked directory on PATH. The archive contains marv, marv-mcp, std/, docs/, spec/, and examples/; the CLI finds the sibling std/ automatically, and agents can read docs/agents.md from the installed toolchain. App repositories do not need to copy this compiler repository.

my-marv-app/
  marv.toml
  src/main.mv

Use the compiler repository only when developing the compiler itself:

git clone https://github.com/joaoh82/marv-lang
cd marv-lang
make build            # cargo build --release  → ./target/release/marv
make test             # cargo test --workspace (z3-backed verify tests run if z3 is present)

Then drive the toolchain (examples ship in examples/):

marv fmt examples/factorial.mv                      # canonical form (the parser's inverse)
marv check examples/factorial.mv                    # type / effect / capability / error / linearity
marv run examples/factorial.mv --entry factorial 6  # 720  (tree-walking interpreter — the oracle)
marv build --run examples/factorial.mv --entry factorial 6   # 720  (Cranelift JIT)
marv build examples/factorial.mv --entry factorial --out factorial && ./factorial 6
marv build --emit object examples/factorial.mv --entry factorial -o factorial.o
marv build --target native-llvm --run examples/factorial.mv --entry factorial 6
marv build --target wasm-component examples/factorial.mv -o factorial.wasm  # + factorial.wit
marv verify examples/clamp.mv                       # proved  (Tier-2 SMT) — or a counterexample
marv commit examples/clamp.mv                       # freeze into the content-addressed store

(Or run any of these via cargo run -p marv-cli -- <args> without installing the binary.)

web/ is a dependency-free demo proving capability-gated sandboxing: a pure module imports nothing, while a module that wants the network imports Net and cannot be instantiated unless the page grants it.

make build && marv build --target wasm-core examples/factorial.mv -o web/factorial.wasm
cd web && python3 -m http.server 8087   # open http://localhost:8087/

marv is the CLI front end; the agent-facing half is the JSON-RPC service (marv-server).

Both .mv source and *.core.json Core-IR snapshots are accepted. See docs/cli.md for full details and exit codes.

The toolchain is built for this loop (spec/03 §5): an agent owns an in-memory snapshot, checks it, applies the highest-confidence fix a diagnostic carries (or regenerates the offending definition), formats, verifys the verified-subset definitions, builds/runs with a chosen capability grant, and commits — freezing reproducible hashes and skipping re-audit of code whose hash was already reviewed.

marv is designed to be driven by LLMs/agents. Start with docs/agents.md — how to drive the toolchain: the generate→check→repair loop, the CLI commands, the capability model, and the invariants. The repo's agent-instruction files (AGENTS.md for Codex/Cursor, CLAUDE.md for Claude Code) carry the contributor rules and point there. For tool-call access, the MCP server (crates/marv-mcp) exposes the JSON-RPC protocol methods as MCP tools; see docs/agents.md for wiring it into Claude Code, Codex, and other MCP clients, plus the bundled Claude Code skill.

crates/
  marv-syntax/       lexer, recursive-descent parser, AST, canonical formatter
  marv-core/         Core IR (ANF + de Bruijn), lowering, blake3 content hashing
  marv-types/        type / effect / capability / error-set / reference / linearity checker
  marv-db/           salsa incremental query database (the protocol's backbone)
  marv-verify/       SMT contract discharge (z3 via easy-smt) for the verified subset
  marv-codegen-cl/   Cranelift backend (native JIT + AOT object/executable)
  marv-codegen-llvm/ LLVM IR backend (clang-driven first release slice)
  marv-codegen-wasm/ WebAssembly backend (capabilities as host imports)
  marv-interp/       tree-walking interpreter (the semantics oracle)
  marv-store/        content-addressed store + lockfile (Merkle DAG, free renames, dedup)
  marv-server/       JSON-RPC agent-protocol server (wraps marv-db queries)
  marv-mcp/          MCP server exposing the protocol to agents
  marv-cli/          the `marv` command-line front end
std/                 the standard prelude, written in marv
selfhost/            Stage-1 self-hosting (compiler passes ported to marv)
examples/            illustrative .mv programs (kept in canonical form)
web/                 the WebAssembly capability-sandbox browser demo
spec/                normative design specs (read these first)
docs/                human-facing toolchain documentation
tests/               repository-level golden / round-trip / differential fixtures

• Specs (normative): spec/01 (design), spec/02 (grammar + Core IR), spec/03 (agent protocol). Read in order.
• Toolchain docs: docs/ — CLI, language reference, standard library, platform support, checker, core IR, query server, run & codegen, verification, store, agents.

Stage-0 milestones M0–M7 are complete. The language surface the parser accepts is a deliberate growing subset (today: fn/struct, enum/match, error/!T/? error handling, interface/impl + generics, capabilities & perform from source (io.fs() narrowing, out.write(...) → Perform, inferred effect rows checked against the capability parameters), struct literals + indexing + assignment, char literals + as casts + len, string concat/slice/index/iteration/building, std.collections.List[T] with explicit-Alloc growable operations, explicit-allocation List/Set/Map collection literals, std.collections.Map[K, V] / Set[T] with string-key compatibility plus scalar i64 hash-backed operations, a first std.iter.Iter[T] protocol-backed iterator wrapper, std.bytes byte-slice and UTF-8 helpers, std.json scalar/flat-object plus recursive/materialized JSON parsing and serialization, the first std.http request/response helper layer over explicit Http authority, an explicit HTTP listener/router surface (Net.listen → Listener.accept_http → Http.respond), the first std.spawn scoped task-handle layer over explicit Spawn authority, unsafe fn audit metadata plus unsafe extern fn host FFI declarations with required SAFETY: comments and unsafeSites, while/for loops, let/var, if/else, arithmetic/boolean ops, the prefix unary operators (-e, not e, &e/&mut e), calls/recursion, pure + requires/ensures contracts). Local non-std source imports now lower/check/run/build as module sets, marv.toml packages can declare source roots and local path dependencies, marv/openPackage opens those packages for agents, and the content store supports lockfile-pinned cross-module builds by hash. MARV-48's first application-language wave is complete; the remaining post-MARV-48 roadmap covers host-backed socket serving beyond the deterministic listener harness, executable host FFI bindings, WASM component packaging, native capability-host runtime coverage, and deeper verification. The first Stage-1 self-hosting milestone is also in place: selfhost/driver.mv sequences marv-written parser and lower/check slices over a documented tiny corpus while Rust Stage 0 remains the oracle and fallback. The full backlog (surface growth → backend breadth → verification breadth → application runtime → packaging/LLVM → self-hosting) — with phases, ordering, and the dependency graph — is in docs/roadmap.md, mapped to the MARV-# tasks in the project tracker.

• make fmt-check && make clippy && make test must pass (CI enforces this; the toolchain is pinned in rust-toolchain.toml).
• examples/, tests/, and docs/ are first-class — update them in the same change that alters observable behavior. See CLAUDE.md for the engineering invariants.
• Maintainers: see MAINTAINERS.md.

Dual-licensed under either of MIT or Apache-2.0 at your option.