levain-cli

The open toolchain for authoring Levain agent recipes: a validator, model checker, and code generator for the recipe formats that Levain agents are defined in.

A recipe package is one of two kinds, set by kind under [tool.levain] in its pyproject.toml:

• graph (the default): a graph.tla PlusCal spec (the agent's node graph and state) plus a Python package with one function per node.
• harness: one engine session (Claude Code or Hermes) declared in [tool.levain.harness]: engine, model, effort, system prompt, tools, MCP servers and state fields. No graph and no Python.

This tool checks both and keeps a graph's two halves coherent:

• validate — parse a spec, enforce the recipe grammar profile, check graph topology, translate PlusCal to TLA+, and model-check the result with TLC (deadlock and termination).
• validate-package — validate a package of either kind. For a graph: all of the above, plus Python source cross-checks (every @node function exists and is importable) and pyproject.toml checks. For a harness: the [tool.levain.harness] keys and values, the prompt file, the state fields and the MCP server names.
• generate-state — regenerate _state.py, the typed GraphState TypedDict a graph's node functions program against. A harness has no state module.

Install

uv tool install levain-cli

TLC model checking (stages 4-5) needs a Java runtime; tla2tools.jar is fetched automatically on first use. Without Java the tool degrades to the pure-Python stages and says so — the Levain platform re-runs full validation on every push, so nothing is lost, only local feedback latency.

Use

levain validate graph.tla
levain validate-package .
levain generate-state .
levain --version

The import package is levain_recipe — use it to lint recipes from your own CI or scripts:

from levain_recipe.validate import validate_fast, validate_recipe

validate_recipe(dir) reads the package's kind and returns a ValidatedSpec for a graph or a HarnessSpec for a harness, or a list of errors.

Validation errors are prescriptive ([stage] line N: message, with TLC counterexample traces) — they are the recipe format's primary teaching interface, for humans and agents alike.

For MCP clients that cannot run shell commands (e.g. Claude Desktop), levain mcp serves the same operations over stdio; install with the [mcp] extra.

What this is not

Recipe execution — compiling a validated spec into a running agent, sandboxing, integrations — happens on the Levain platform. Passing local validation is necessary, not sufficient: the platform validates again server-side before a version can be published.