Command line

@artano-ai/cli puts the engine in a shell. It exists for the one place the other surfaces could not reach: a CI pipeline, where a wrong number should fail a build without a human reading anything.

Install

npm install -g @artano-ai/cli

Or run it without installing:

npx @artano-ai/cli cards list

The only runtime dependency is the engine itself — argument parsing uses Node’s built-in parseArgs, so nothing else comes along for the ride.

Verify a finished output

lemma verify free-fall-uniform-gravity --output '{"gEarth_m_per_s2": 9.81}'

USCE · free-fall-uniform-gravity · Free fall in uniform gravity (no air resistance)
  pass  gEarth_m_per_s2 = 9.81 is within [9.79, 9.83].
— 1 of 1 checks passed · severity NONE
All checked values fall within the card's validation envelopes.

Read the values from a file or a pipe instead of inline:

lemma verify ideal-gas-law --output-file results.json
my-simulation | jq '{gasConstant_J_per_molK: .R}' | lemma verify ideal-gas-law --output-file -

Values must be finite numbers. A quoted "9.81" is refused, not coerced — a verdict should never depend on a conversion you did not ask for.

Three shapes of evidence

--output is one of three. A run can present any combination, and they report as one verdict, because they describe one run:

Flag	Evidence	Checked against
`--output` / `--output-file`	scalars	`validationEnvelopes`
`--series`	samples of one or more quantities	`seriesConditions`
`--refinement`	`[h, error]` levels	the card’s declared convergence order

--series reaches cards nothing else can. A density of states has no system-independent range, so density-of-states deliberately declares no envelopes — but it cannot be negative in any material:

$ lemma verify density-of-states --series dos.json
  fail  g >= 0 is violated by 1 of 5 covered samples; the worst is -0.4 at index 1.
        This is not a tolerance question — the quantity is outside its own definition.

where dos.json is {"epsilon": [...], "g": [...]}.

--refinement recomputes a convergence order instead of trusting a reported one. Given [[0.1, 1e-5], [0.05, 2.5e-6], …]:

$ lemma verify finite-difference-truncation-error --refinement study.json
  pass  Observed convergence order 2 is within [1.8, 2.2], measured over 4
        refinement levels (per-level: 2, 2, 2).

If the study contains round-off-limited levels it fits a shallower slope and could look like a wrong order. It does not fail — it warns and prints the per-level orders so you can see which level to drop:

  warn  per-level orders are 2, 2, 2, 2, -0.107, spanning 2.11 (> 0.4, declared by
        finite-difference-truncation-error) … a tail that flattens usually means
        round-off-limited levels at small h.

Combining them checks a claim and its evidence together — here the reported order against the envelope, and the measured order against the study:

lemma verify finite-difference-truncation-error \
  --output '{"observedConvergenceOrder": 2.0}' \
  --refinement study.json

Exit codes

Code	Meaning
`0`	checked, and it passed
`1`	checked, and a value is out of range
`2`	could not check at all — bad card id, unreadable input, bad usage

The 1 / 2 split is deliberate and worth preserving in whatever wraps this. “The physics is wrong” and “you typed the card id wrong” are both non-zero, but a pipeline that renders them as the same red build teaches people to ignore the red build.

An absent check is not a passing one

By default an output key with no declared envelope is simply not checked, so a run can exit 0 having verified nothing:

$ lemma verify free-fall-uniform-gravity --output '{"someOtherKey": 1.0}'
— 0 of 0 checks passed · severity NONE
No validation envelopes overlapped the provided output keys — nothing to check.

--require-checks makes that a failure:

$ lemma verify free-fall-uniform-gravity --output '{"someOtherKey": 1.0}' --require-checks
— 0 of 0 checks passed · severity HIGH    # exit 1

This is the flag for CI. It is not the default because turning it on would change what every existing green build means — the same reasoning that keeps require_checks opt-in in the SDK.

Cross-check a proposed card

Against the corpus:

lemma crosscheck free-fall-with-linear-drag

Against a draft you are writing — the cheapest place to catch a card that is schema-valid but physically wrong:

lemma crosscheck ./my-new-card.json
cat my-new-card.json | lemma crosscheck -

  fail  Dimensional mismatch — the formula (1/2) m v [J] derives to L·T^-1·M,
        but LHS [E [J]] is L^2·T^-2·M. The proposed equation does not hold
        dimensionally.

A warn does not fail. It means the engine declined to answer: the claim is recorded, neither proven nor refuted. Failing on it would punish authors for writing down claims the engine cannot yet check, and the corpus wants those claims written down. See verdicts.

Browse

lemma cards list                       # every card
lemma cards list --kind hypothesis
lemma cards list --domain physics      # domain prefix
lemma cards show density-of-states
lemma cards search entropy
lemma paths                            # which corpus actually resolved

search is substring matching over ids, names, domains and principles — not semantic search. That is rag_lookup on the MCP server, which needs a vector index.

lemma list and lemma show work as bare aliases too, matching the Python CLI.

Scripting

--json emits machine-readable output and turns colour off:

lemma verify ideal-gas-law --output-file out.json --json | jq '.overall.severity'
lemma cards list --kind principle --json | jq -r '.[].id'

Colour is also off automatically when stdout is not a TTY, and honours NO_COLOR.

In a pipeline

- name: Verify the simulation output against Lemma
  run: |
    npx @artano-ai/cli verify ideal-gas-law \
      --output-file results.json \
      --require-checks

Two runtimes, one binary name

The Python SDK installs a lemma command as well. That is intended — they are the same tool over the same corpus and the same engine contract, so install whichever runtime you already have. verify, crosscheck, list, show and paths exist in both, spelled the same, with the same exit codes. A test suite in each package pins that contract so the two cannot drift apart.

Two differences are deliberate:

crosscheck --symbolic is Python-only. There is no comparable computer-algebra system in the Node ecosystem, so the Python CLI is the only place a declared limit or conservation claim can be proven from a shell rather than recorded. See symbolic verification.
lemma authors and lemma serve are Python-only — the first reads git history, the second starts the MCP server over stdio.

Pointing at a different corpus

LEMMA_CARDS_DIR=./my-cards lemma cards list

Run lemma paths to confirm which corpus resolved before trusting a verdict — a bundled copy can shadow the one you think you are checking against.