ponens

Getting started

ponens turns an AI coding agent's session into a higher-level reasoning record — a curated, verifiable account of what it built and why — then makes the reasoning rigorous and governs it with Computable Governance (machine-checkable best-practice policies). The CLI is terminal-first; the browser is the escalation.

Install

# from this repo
pip install "ponens @ git+https://github.com/imandra-ai/ponens.git#subdirectory=cli"

# or for local development
pip install -e ./cli

The flow: emit a draft from the session, curate the narrative, declare what only the agent can (artifacts, gaps, and the goal it was pursuing), grade and govern it, then view and share. Every command is plain text — greppable, pipeable, --json where you script it. This is the agent / CI surface too.

Looking for a specific task instead of the full tour? See the practical guides — capture & curate a trace, review an AI-generated PR, add ponens to CI, and govern a repo with policies.

1 · Emit — capture the session

An agent emits the trace from its own session transcript; you write nothing. Emission captures the actions, file lineage, decisions, and reasoning as ground truth.

ponens emit -o trace.json                            # newest session for this project
ponens emit transcript.jsonl -o trace.json --from claude-code

2 · Curate the narrative

Emission seeds each step's title from the raw directives ("yes", "ok now fix it"). Those are drafts — rewrite them into a clean account of what was built and why. The atomic actions underneath stay untouched and honest.

ponens trace meta ls trace.json                      # the steps, and how curated each is
ponens trace meta set trace.json m3 --title "Add idempotency to capture" --status completed
ponens trace meta merge trace.json m7 m8             # fold dead-ends into one step
ponens trace retitle trace.json --title "…" --outcome "…"

3 · Declare — what emission can't derive

The produced artifacts (so the lineage DAG is real) and the negative space — the gaps only the agent can declare.

ponens trace artifact trace.json --type VerificationResult --name "no double-charge" --producer-action-id 12
ponens trace residual add trace.json --kind assumption --severity high \
    --statement "Assumes the gateway sends a stable idempotency key" \
    --suggested-check "confirm the retry contract"

4 · Goals & acceptance — declare intent, resolve it

Declare what a change is for and what "done" means: a goal (intent + scope) with typed acceptance items (change / property / obligation / gap). Acceptance adds no new evaluator — each item resolves from evidence already in the trace (a verification result, a policy evaluation, a residual, a diff).

No model decides whether a goal is met — the evidence does. Resolution is deterministic: each binding is matched against the typed artifacts in the trace, and the relevance cone is a walk over the existing lineage — no LLM, no scoring. So every "done" traces to a specific artifact, and re-running it always gives the same answer: progress that is grounded, reproducible, and auditable, not asserted (Trace Spec §18).

ponens trace resolve trace.json --goals goals.json   # each acceptance item's live status
ponens trace enrich  trace.json --goals goals.json -o enriched.json   # + progress, relevance cone, derived stale-evidence gaps
ponens trace residuals trace.json --derived          # declared gaps + computed stale proofs

5 · Grade it

A quality rubric — structure, rationale coverage, negative space, reproducibility, verification evidence, and lineage — plus a separate policy-compliance line. Treat the grade as a hygiene floor to clear, not a number to game.

ponens trace grade trace.json

6 · Govern — Computable Governance

Check the trace against best-practice policies — conformance checks evaluated over the record. A real, automatic gate (exit code), fully offline.

ponens registry update
ponens policies search testing
ponens policies add tests_before_commit --into trace.json
ponens trace check trace.json                        # → PASS / FAIL

7 · View it

Read the reasoning behind the commit — zoom from intent-named steps down to atomic actions, with the lineage DAG, decisions, and the residual surface.

ponens trace view trace.json                         # self-contained page; opens in a browser
ponens trace view trace.json --out trace.html        # write the HTML (e.g. a CI artifact)

Headless (SSH/CI)? It prints the file path instead. See it live in the demo.

8 · Share it

ponens bind && ponens push                           # bind 1:1 to the commit, publish for review

Or post it on the pull request — the grade, the declared gaps, and a one-click interactive viewer — with the pr-trace GitHub Action.

Concepts

  • Trace — the curated, verifiable record of an agent's work session, in two layers: faithful atomic actions (ground truth) and a curated meta-action narrative (spec).
  • Residual surface — what the trace did not establish: assumptions, unverified claims, out-of-scope items, limitations, open questions. It tells a reviewer where to look.
  • Goals & acceptance — what the trace was for and its definition of done: a goal's intent plus typed acceptance items (change / property / obligation / gap) that resolve from the trace's own evidence, so progress is grounded rather than asserted (spec §18). The positive-target dual of the residual surface.
  • Computable Governance — best-practice policies as machine-checkable rules over the trace, written in LTLf extended with scoped-past and structural operators. Browse the gallery, read the Policy Language reference, or write your own.
  • Review handoff — how a reviewing agent consumes a trace: verify the consequential claims, triage the declared gaps, hunt the undeclared ones.