Skip to content

CLI_GUIDE.md

Latest commit

 

History

History
218 lines (163 loc) · 10.7 KB

CLI_GUIDE.md

File metadata and controls

218 lines (163 loc) · 10.7 KB
Raw

CLI and E2E Guide

Examples

The examples/ directory contains sample .mm files with known verification failures for testing the self-healing loop:

File Violation Type Description
examples/sword_test.mm Precondition Division without b != 0 guard
examples/effect_test.mm Effect mismatch Uses FileWrite but only declares [Log] 
# Demo: precondition fix
uv run mumei-agent heal examples/sword_test.mm

# Demo: effect mismatch fix
uv run mumei-agent heal examples/effect_test.mm

# Backward compatible (no subcommand = heal mode)
uv run mumei-agent examples/sword_test.mm

Generate Mode

The generate subcommand creates new Mumei code from a JSON specification. It uses an LLM to generate code, then verifies it with mumei check and mumei verify --json, auto-fixing any issues.

Spec JSON Format

{
  "name": "safe_read",
  "params": [{"name": "path", "type": "Str"}],
  "effects": ["SafeFileRead(path)"],
  "requires": "starts_with(path, \"/tmp/\") && not_contains(path, \"..\")",
  "ensures": "result >= 0",
  "description": "Read a file safely with path traversal prevention"
}

Usage

# From a spec file
uv run mumei-agent generate --spec-file spec.json --output out.mm

# From inline JSON
uv run mumei-agent generate --spec '{"name": "add", "params": [{"name": "a", "type": "i64"}, {"name": "b", "type": "i64"}], "requires": "true", "ensures": "result == a + b"}' --output add.mm

# With metrics output
uv run mumei-agent generate --spec-file spec.json --output out.mm --metrics

Metrics

Use the --metrics flag to output a JSON summary of generation/fix statistics:

{
  "total_attempts": 3,
  "successes": 1,
  "by_violation_type": {
    "generation": {"attempts": 1, "successes": 1},
    "effect_mismatch": {"attempts": 2, "successes": 0}
  }
}

E2E Demo

e2e_demo.mp4

The self-healing loop follows this interaction flow:

  1. Verification failure: mumei build detects a precondition bug (missing b != 0 guard)
  2. LLM fix: The agent sends the Z3 counter-example to the LLM, which generates a corrected requires clause
  3. Re-verification: mumei build confirms the fix passes formal verification

Spec-to-Verified-Code E2E Demo

The examples/run_e2e_demo.py script demonstrates the full pipeline: specification JSON -> LLM code generation -> mumei verify -> self-healing loop -> verified output.

# Dry-run mode (validate spec only, no LLM or mumei required)
python -m examples.run_e2e_demo --dry-run
python -m examples.run_e2e_demo examples/simple_add_spec.json --dry-run

# Full pipeline (requires LLM API key and optionally mumei binary)
python -m examples.run_e2e_demo                                # uses e2e_demo_spec.json
python -m examples.run_e2e_demo examples/simple_add_spec.json  # minimal example

Available spec files:

File Description Effects
examples/e2e_demo_spec.json Fetch GitHub user via HTTPS SecureHttpGet
examples/simple_add_spec.json Add two non-negative numbers None

P11 Natural-language Specification Extraction

See docs/NL_SPEC_DEMO.md for a recorded field demo of uv run mumei-agent extract-spec, including bank-transfer, RegTech KYC, and spec-extraction-to-code-generation examples with mumei verify output.

Use contradiction-only mode when you want to validate natural-language requirements before generating code:

uv run mumei-agent extract-spec \
  --text "x must be greater than 0 and less than 0" \
  --domain math \
  --output contradiction-report.json \
  --check-contradiction-only

This extracts the forge-task spec, builds temporary trusted atoms from the extracted contracts, runs Mumei spec satisfiability, and writes contradiction_found, natural_language_explanation, and the raw verification payload to the output JSON. It skips .mm code generation and self-healing entirely.

p11_live_extraction_e2e.mp4

A live OpenAI extraction E2E recording is available at docs/p11_live_extraction_e2e.mp4.

LLM Provider Support

Provider Config Pattern Cost
Ollama (local) Pattern 1 Free
External API (DashScope etc.) Pattern 2 Pay-per-use
vLLM (local) Pattern 3 Free
OpenAI Pattern 4 Pay-per-use

See .env.example for configuration details.

Subcommands

Command Description Example
heal (default) Self-healing loop for existing .mm files uv run mumei-agent heal examples/sword_test.mm
self-correct P9-F Loss Vector driven self-correction loop uv run mumei-agent self-correct examples/effect_test.mm --max-iterations 3
generate Generate new .mm code from spec JSON uv run mumei-agent generate --spec-file spec.json --output out.mm
audit Audit existing code or directories: extract spec, check health, verify contracts, detect cross-validation gaps uv run mumei-agent audit --code-file src/ --auto-migrate --auto-heal
migrate-suggest Generate .mm migration skeletons for functions with verification issues uv run mumei-agent migrate-suggest --code-file src/foo.ts --language typescript
publish Autonomous delivery: generate → verify → emit wrappers → PR uv run mumei-agent publish --spec examples/publish_demo/payment_spec.json --dry-run
forge Autonomously extend the mumei std library with verified atoms uv run mumei-agent forge --tasks-dir forge_tasks/ --mumei-repo ../mumei --max-tasks 1
validate-spec Cross-validate natural-language specs for contradiction, ambiguity, over-constraint, and Z3 satisfiability uv run mumei-agent validate-spec --input spec.txt --format nl
validate-code Infer and verify contracts from existing code (Python, Rust, TypeScript, Go). --language is optional; inferred from extension when omitted uv run mumei-agent validate-code --input code.ts
validate-spec-to-code Detect missing implementation constraints by comparing specs to code uv run mumei-agent validate-spec-to-code --spec spec.txt --code src/foo.py --language python
validate-code-to-spec Detect spec drift by comparing changed code to specs uv run mumei-agent validate-code-to-spec --code src/foo.py --spec spec.txt --language python
verify-conformance Produce the V1-C spec→code conformance matrix and next_steps-first report uv run mumei-agent verify-conformance --spec spec.txt --code src/foo.py --language python --format human (python|rust|typescript|go)
verify-traceability Combine V1-C conformance and V1-D drift into one bidirectional traceability summary uv run mumei-agent verify-traceability --code src/foo.py --spec spec.txt --language python --format human (python|rust|typescript|go)
extract-spec Extract forge spec from existing code or natural-language input uv run mumei-agent extract-spec --code-file src/foo.py
check-spec-health Check a Mumei spec for contradictions, over-constraints, and vacuity uv run mumei-agent check-spec-health spec.mm
cross-validate Cross-validate spec↔code consistency across multiple files uv run mumei-agent cross-validate --spec spec.txt --code src/foo.py
proliferate Autonomous weekly loop: analyze gaps → spec → generate → blast-radius check → heal → PR uv run mumei-agent proliferate --mumei-repo ../mumei --max-proposals 3
propose Generate forge task specs from analyze-std-gaps output uv run mumei-agent propose --auto --mumei-repo ../mumei
analyze-std-gaps Identify gaps in std/ coverage uv run mumei-agent analyze-std-gaps --mumei-repo ../mumei
health Show agent health status (LLM provider, mumei binary, etc.) uv run mumei-agent health
mcp-server Run mumei-agent as a FastMCP server (forge / heal / health / propose tools) uv run mumei-agent mcp-server

Verification Workflow Guide

ユースケース別の検証手順（自然言語仕様の矛盾チェック、既存コードの検証、仕様↔コード整合性検証、人間向け操作ガイド）は docs/VERIFICATION_WORKFLOW_GUIDE.md を参照。

Forge Mode

forge extends the mumei standard library with new verified atoms described in task spec JSON files.

# Preview the execution plan without running anything
uv run mumei-agent forge --tasks-dir forge_tasks/ --mumei-repo ../mumei --dry-run

# Run a single spec (path is looked up relative to --tasks-dir)
uv run mumei-agent forge --mumei-repo ../mumei --task vstd_safe_add.json

# Bias the queue toward the weakest P16 benchmark categories' stdlib domains
uv run mumei-agent forge --mumei-repo ../mumei --max-tasks 2 \
  --benchmark-feedback /tmp/forge-feedback.json

# Run the whole queue, capped at 5 tasks per invocation
uv run mumei-agent forge --tasks-dir forge_tasks/ --mumei-repo ../mumei --max-tasks 5

Each task spec declares a target_file inside the mumei repo, a mode (append, create, or replace), and one or more atoms. The orchestrator drives generate_code() + mumei verify --json + self-healing, appends (or creates/replaces) the target .mm file, optionally git-commits the change, and records the outcome to forge_log.json. Already-completed task_ids are automatically skipped on subsequent runs.

Create/replace tasks whose atoms provide explicit body values and set deterministic_bodies: true are rendered deterministically without requiring an LLM credential; vstd_core_predicates.json and vstd_crypto_primitives.json exercise this no-LLM path.

See forge_tasks/README.md for the full task spec schema.

Benchmark Feedback (P16-C)

The mumei benchmark suite can drive vStd prioritisation:

# In the mumei repo: score each benchmark category and emit the feedback doc
python3 benchmarks/run_benchmarks.py --forge-feedback /tmp/forge-feedback.json

# In mumei-agent: bias gap proposals / forge tasks toward weak domains
uv run mumei-agent proliferate --mumei-repo ../mumei \
  --benchmark-feedback /tmp/forge-feedback.json \
  --output-json /tmp/proliferate/summary.json

The mumei.benchmark_forge_feedback/v1 document carries a per-category weakness_score (expected-outcome match rate, counterexample catch rate, trusted ratio, plus Z3 / Lean solver-time signals) and the resulting negative priority_delta per stdlib domain. Feedback only reorders work that gap analysis already produced — it never adds or drops proposals — and the applied bias is recorded under benchmark_feedback in the run summary JSON. A missing or malformed document is logged and ignored so the loop still runs.