← Guides

Use ponens programmatically

You'll end up with policy compliance you can drive from your own tool — a machine-readable checker you can call on every change, in-process evaluation from Python, and a live compliance state that updates as work happens. No server: the checker is pure, local, and deterministic.

ponens evaluates LTLf policies over a trace. The same evaluator that powers ponens trace check is exposed two ways — a JSON-emitting CLI and a Python function — so a build step, an editor extension, or a CI job can ask "does this trace comply?" and act on the answer.

pip install -U ponens        # or: uv pip install -U ponens / pipx upgrade ponens

Grab a trace to try this on

ponens ships real sample traces — machine-checked proofs, decompositions, conformance runs. List them and pull one down, so every command below runs against an actual trace:

ponens demos list
ponens demos get stripe_v1_1.json -o trace.json

1. Check a trace, get JSON back

--json makes the checker machine-readable: it prints the policy_evaluation records (one per policy) and nothing else, so you can pipe it straight into your tool.

ponens trace check trace.json --json

[
  { "policy_id": "formalize_before_verify",            "status": "passed", "checked_at_action_id": 42 },
  { "policy_id": "decomposition_drives_tests",         "status": "passed", "checked_at_action_id": 42 },
  { "policy_id": "reasoning_required_for_high_stakes", "status": "failed", "checked_at_action_id": 42 }
]

Each record carries the policy_id, a status (passed / failed / unknown / not_applicable), the action position it was checked at, and an optional note. A trace with no policies prints [].

2. Stamp the results into the trace

--write evaluates and writes the policy_evaluations array back into the trace file in place — so the trace becomes self-describing (it carries both its policies and their latest results, ready for the viewer or an audit).

ponens trace check trace.json --write

3. Evaluate in-process (Python)

Skip the subprocess entirely — call the evaluator directly. It's a pure function over a trace dict, so you can score policies inside your own pipeline.

from ponens.trace import evaluate_policy, normalize_trace
import json

trace = json.load(open("trace.json"))
normalize_trace(trace)                       # resolve artifact/output links

for policy in trace["policies"]:
    status, note = evaluate_policy(policy, trace)
    print(policy["policy_id"], status, note or "")

evaluate_policy(policy, trace) returns (status, note). A policy is just an object with a name, a severity, and an LTLf formula — you can hand-write one, or pull it from the gallery (next).

4. Connect gallery packs

Discover packs and pull their policies (with formulas) from the configured sources — the community gallery, or a local one you add to .ponens/sources.toml.

# list available packs
ponens search --type pack --json

# a pack's policies, ready to embed in a trace's "policies" array
ponens search --json | jq '.policies[] | select(.pack == "apply-formal-methods")'

Attach the ones you want to your trace's policies list, then run ponens trace check. That's the whole loop: select packs → embed → check. The apply-formal-methods pack, for example, requires that high-stakes code is formally analyzed and that decompositions drive tests.

5. A live per-change compliance loop

Putting it together: re-check on every change and keep a compliance state that's always current. An editor integration or a formal-reasoning agent can call the checker after each change and update its compliance view from the result.

import json, subprocess

def recompute_compliance(trace_path):
    """Call the native checker; return the fresh policy_evaluations."""
    out = subprocess.run(
        ["ponens", "trace", "check", trace_path, "--json"],
        capture_output=True, text=True,
    ).stdout
    return json.loads(out or "[]")

# ... on every artifact / commit / save:
evaluations = recompute_compliance("trace.json")
failed = [e for e in evaluations if e["status"] == "failed"]
if failed:
    print("policy violations:", [e["policy_id"] for e in failed])

"Where it makes sense": a data-driven high-stakes surface

The high_stakes_path predicate — used by policies like reasoning_required_for_high_stakes — matches an action's target against the trace's high_stakes_paths. Set it from whatever decides which code warrants formal methods (a target scan, a CODEOWNERS-style list, a risk register):

{
  "trace_id": "...",
  "high_stakes_paths": ["billing/", "auth/", "payments/"],
  "policies": [ /* ... */ ],
  "actions": [ /* ... */ ]
}

Now "apply formal methods where it makes sense" is decided by evidence in the trace, not a hard-coded path list — and every check re-evaluates against the current surface.

← Back to guides · Writing policies →