Verify existing code and specifications with formal methods — before you write .mm.
Mumei is a formal verification toolchain that starts from existing code, natural-language requirements, or .mm modules. It uses Z3, proof certificates, and AI-agent workflows to find bugs, spec drift, and contradictions, then helps move critical logic into checked .mm code.
Technical Paper — proof-driven programming architecture, autonomous verification loop, and case studies.
Verified Local Agents: When AI Code Generation Meets Formal Proof — a high-level overview of the Mumei Forge, Z3/Lean pipeline, and case studies (Medium).
existing code / natural language spec → MCP or mumei-agent → Z3-backed diagnostics → optional
.mmmigration → LLVM / proof artifacts
Release and Homebrew artifacts include per-module proof certificates and the
aggregate proof bundle. Consumers can re-verify packaged sources with
mumei verify-cert <certificate> <source.mm> --strict.
Run uv run mumei-agent audit --code-file ... --auto-migrate --auto-heal, or MCP scan_and_fix, before asking users to author .mm files. See docs/CROSS_PROJECT_ROADMAP.md, docs/ROADMAP.md, and docs/ONBOARDING.md for the contract, vocabulary, V1-A〜E order, Lean escalation, and PR evidence.
Recent standard-library and mumei-lean sync points are tracked in the Standard Library Reference.
mumei-agent verifies existing code and specifications before migration. See docs/ONBOARDING.md and the Verification Workflow Guide.
git clone https://github.com/mumei-lang/mumei-agent
cd mumei-agent
cp .env.example .env # Set LLM_BASE_URL / LLM_API_KEY / LLM_MODEL
uv sync
# After this, run commands as uv run mumei-agent <subcommand>1. Find likely bugs in existing code
uv run mumei-agent validate-code --input src/payment.py2. Detect spec↔code drift
uv run mumei-agent validate-spec-to-code --spec docs/spec.txt --code src/payment.py3. Find contradictions in specs only
uv run mumei-agent validate-spec --input docs/spec.txt --format nl- Step 0: Audit existing assets without
.mm:uv run mumei-agent audit --code-file src/payment.py --auto-migrate --auto-heal - Step 1: Write a critical contract and verify it:
mumei verify specs/payment.mm - Step 2: Implement new logic in
.mmand emit artifacts:mumei build src/main.mm -o dist/output
MCP clients use scan_and_fix for the same audit → migrate-suggest → heal route. The cross-spec artifact vocabulary and migration guidance are in docs/CROSS_SPEC_GUIDE.md.
Mumei is Module B (AR) in the four-repository NLAE pipeline: it reconstructs contracts into Z3 obligations and returns a Loss Vector for self-correction and Lean fidelity checking.
mumei-agent → generated .mm → mumei → Loss Vector JSON → self-correct → mumei-lean → mumei-demo
See docs/CROSS_PROJECT_ROADMAP.md § P9 for phase status, artifacts, feedback fields, and E2E workflow.
With cargo build --features otel and OTEL_ENABLED=true, mumei verify exports OTLP spans and propagates TRACEPARENT across the mumei-agent → Rust → Z3 path. The feature is zero-cost when disabled and degrades gracefully without a collector. Details and CI coverage: docs/ROADMAP.md § P15 and .github/workflows/otel-tracing.yml.
curl -fsSL https://mumei-lang.github.io/mumei/install.sh | bash
brew install mumei-lang/mumei/mumei
curl -fsSL https://mumei-lang.github.io/mumei/install.sh | bash -s -- --version v0.6.18See Releases for older versions. No Rust toolchain is required; OS/arch is detected automatically.
Build from source
brew install llvm@17 z3 # macOS
sudo apt-get install -y libz3-dev llvm-17-dev libclang-17-dev # Linux
cargo build --release
cargo install --path .
mumei setup && source ~/.mumei/envThe complete CLI command table is in docs/TOOLCHAIN.md, MCP tools and setup are in docs/MCP.md, and the full project structure is in docs/ARCHITECTURE.md.
| Document | Content |
|---|---|
| Verification Workflow Guide | Natural-language spec validation, existing-code verification, spec↔code alignment, and human-friendly operation guide |
| MCP Integration | MCP tools, setup, and multi-agent collaboration |
| Language Reference | Types, generics, traits, ownership, async |
| Features | Feature matrix formerly summarized in this README |
| Standard Library | Option, Result, List, BoundedArray, sort |
| Examples & Tests | Verification suite, .mm code samples, and negative tests |
| Architecture | Compiler internals and repository structure |
| Report Schema | report.json, semantic feedback, and rich diagnostics JSON |
| Cross-Spec Verification | System-wide contract consistency, invariants, and dependency cycles |
| Toolchain | CLI commands, package management, CI/release |
| Onboarding Guide | Gradual path from existing code and natural language to .mm |
| LSP Integration | Editor CodeLens, intent drift, spec-code mapping, and mumei-agent spec/code diagnostics |
| LSP Diagnostic Data | Cross-editor diagnostic and CodeLens data contract |
| MCP Tool Contract | Canonical mumei-forge and mumei-agent tool signatures |
| Roadmap | Strategic roadmap |
| Capability Security | Effect-based capability security evaluation |
| Changelog | Release history |
| Diagnostics | Multi-span diagnostics, compound constraint decomposition |
| Meta-Architect | Contract conflict analysis and interface refactoring tools |
| Plugin Guide | Emitter plugin development |
| Proof Certificate | Proof certificate schema and usage |
| Spec Guide | Spec-writing guidelines for Z3-decidable fragments |
| FFI | Foreign function interface (Rust/C) |
| Concurrency | Async/await and deadlock-free resource hierarchy |
| Editors | VS Code and LSP editor integration |
| Patterns | Design patterns and idioms |
| Trusted Atoms | trusted/unverified atom usage |
| Structured Feedback Schema | P9-E structured feedback JSON schema |
| Cross-Project Roadmap | mumei + mumei-agent ecosystem roadmap |
| Claude Code Quickstart | Quickstart guide for Claude Code users |