v1.7.1

Added

• ponens policies lint — validate policies without a trace — lint a policy file locally
  (ponens policies lint policies.json [--json]): required fields, the severity/scope vocabularies,
  and formula syntax, using exactly the oracle trace check applies before evaluating — a policy that
  lints valid can never come back syntax-invalid at check time. Errors are structured
  ({message, path}, the path into the formula's operator tree), so authoring tools can surface them
  in place. With --json the exit code is 0 whenever linting ran and the per-policy verdicts are in
  the records (machine mode, mirroring trace check --json); without it, a human-readable report that
  exits 1 if anything is invalid. Accepts the same file shapes as trace check --policy-file (a JSON
  array, or {"policies": [...]}).

Fixed

• Stale-proof detection keys on the latest proof — a symbol's proof is stale iff its latest
  proof predates the latest change to that symbol, so a property re-proved after an edit heals its
  stale-evidence residual instead of the superseded proof staying reported stale forever. A refutation
  surfaces as the live blocked issue it is, never as staleness. The at-risk guard now reads two
  independent signals: a change recorded on the trace (structural), and artifact_freshness
  re-hashing that catches an on-disk edit the trace has no Diff for.

v1.7.0

Added

• Residuals are first-class artifacts (Trace Spec v1.8) — a residual (an assumption relied on, a
  claim left unverified, an out-of-scope item, a known limitation) is now an artifact_type: "Residual"
  anchored into the lineage DAG via derived_from / target, so the trace's negative space hangs off
  exactly the artifact it qualifies instead of floating in a separate list. The legacy top-level
  residuals[] is still read - and migrate_residuals folds an old trace forward - so existing traces
  keep working. See the new TRACE_SPEC_v1_8 spec.
• Residual-surface policies — a policy can now quantify over the residual surface (e.g.
  no_open_critical_residuals): enrich evaluates it and reports its witnesses - the concrete residuals
  that satisfy or violate it - so a governed goal can require its gaps be closed, not merely that its
  evidence exists.

Changed

• Policy failures point at where they fail — a structural policy evaluation now returns a witness
  record (ev_actions / vi_actions / ev_artifacts / vi_artifacts): the concrete action and
  artifact ids that support or violate it, instead of a bare pass/fail. A failed policy can name the
  exact steps or artifacts at fault.

Fixed

• Decomposition criteria now resolve against a real decomposition — a goal criterion asking for
  Decomposition evidence matched nothing, because a region decomposition is recorded on the trace as
  StateSpaceAnalysisResult. Resolution now canonicalizes artifact-type spellings
  (Decomposition ≡ StateSpaceAnalysisResult ≡ Decomp), so a decomposition criterion ticks when the
  decomposition exists.
• Criteria bind when the engine renamed the symbol — a criterion's component may now carry both a
  source function (the author's name, for display) and a formal symbol (the name the engine gave the
  formalization, e.g. source clamp formalized as clamp_decomp), and resolves on either. A goal no
  longer stays todo just because the proof was recorded under the engine's symbol rather than the
  source name.

v1.6.0

Added

• Goal contracts — an acceptance criterion is now a typed evidence requirement over a code
  component (verification, tests, or decomposition), and a goal carries its own policy bar.
  State the goal as a contract - accomplish these things, subject to these policies - and
  ponens trace enrich returns three independent verdicts: met (criteria resolved from evidence),
  governed (the goal's policies held), and certified (a non-doer confirmed the criteria were
  the right ones). Author the whole contract in one shot with ponens trace goal set --json. See the
  new GOAL_CONTRACT_v0_1 spec.
• Goal-scoped policies — the governed axis — a goal can name policy packs and policies; they
  block by default unless explicitly disabled (recorded on the trace, never silent). Pack names
  resolve against the registry, and enrich attaches the governance result per goal.
• Artifact lineage / provenance API — a new dependency-free ponens.lineage module answers what a
  specific artifact was derived from: ancestor_ids, lineage_types, source_symbols, autoformalized,
  decomposition_backed, and a one-call provenance summary.

Changed

• ponens agent now teaches the goal-contract workflow — typed criteria, the goal's policy bar, and
  the three axes (met / governed / certified), including the rule that the agent proposes the rigor bar
  while a human selects it, and never self-certifies.
• ponens trace enrich now reports the governed axis alongside met and certified.

Fixed

• Goals now reach met when the work is real — a typed criterion resolves by artifact lineage
  (does a proved result for this property trace back to a model autoformalized from this component?)
  instead of matching the verification goal's description text. This fixes goals that never ticked even
  though the property was proved, and stops a similarly-worded but unrelated result from satisfying a
  criterion.

v1.5.0

Added

• Goal authoring from the CLI — a new ponens trace goal command group brings the desktop's goal
  workflow to the CLI, so every trace operation can be done from the command line: set (declare the
  intent + definition of done, or load one via --json), accept (add an acceptance item bound to
  evidence), certify (record a non-doer's sign-off — the certified axis), drop / rm (remove an
  item or a goal), and ls (show each goal's resolved status + met/certified/weakly-specified). Goals
  are written in the spec's snake_case shape.

Fixed

• PyPI project page — the package now ships a README (readme in pyproject.toml), so the PyPI
  project page renders a description instead of "The author has not provided a project description."

v1.4.1

Added

• Faithfulness grading in enrich — ponens trace enrich now grades each goal's definition of
  done (GOAL_FAITHFULNESS_v0_1), not just its progress: met (required criteria resolved from the
  trace's own evidence) vs certified (a reviewer other than the doer approved the criteria, every
  intent clause is covered, and the definition is not weakly specified), plus weakly_specified and
  uncovered_clauses per goal. The trace summary gains goals_met / goals_certified /
  goals_weakly_specified counts.
• Faithfulness gate in trace check — the checker reports each goal's met/certified status and,
  under --strict, fails on the deficiencies the agent controls: a weakly-specified definition
  (nothing proved or policy-checked backs "done") or an uncovered intent clause. "Met but not
  certified" is surfaced as a warning — certification needs a human, so it is never a hard failure.

v1.4.0

Added

• Goal faithfulness — met vs certified — a goal's "done" is now graded on two orthogonal
  axes: met (its acceptance criteria resolved from the trace's own evidence) and certified (a
  reviewer other than the agent confirmed those were the right criteria). The new
  GOAL_FAITHFULNESS_v0_1 spec (under /spec) refines Trace Spec §18 with authorship
  (intent_author, per-item author), clause coverage (intent_clauses + covers), and a
  criteria_review. It guards the principal–agent seam where the agent both authors and meets its
  own definition of done — an honest resolution can still "succeed" against a bar set too low.
• Goals view in the visualizer — ponens trace view now shows a trace's declared goals with their
  acceptance criteria and renders the faithfulness signals inline: Met / Certified badges, a
  weakly-specified warning (a goal backed only by code edits, with nothing proved or policy-checked),
  uncovered-intent-clause warnings, and the intent→criteria authorship seam. Each acceptance
  criterion's evidence chip is a link — click it to jump to the backing artifact in the lineage graph
  (or, for a policy obligation, the Policies view).

Changed

• Richer flagship demo — the Stripe payment-flow trace is now the default demo: a declared goal
  with a certified definition of done, a seven-step meta-action narrative (formalize → catch the amount
  bug with a counterexample → fix → prove both new controls individually and together → conformance →
  ship), full lineage, and three honestly-declared residuals. The bundled sample_payment_idempotency
  trace also gained a declared goal, so the Goals view is populated out of the box.
• Goal-oriented framing on the site — the "not another tracing tool" comparison is reframed as
  descriptive (OpenTelemetry / Langfuse record what happened) vs evaluative (ponens judges each
  trace against its declared goal and its policies), and the header version badge now links to
  /whats-new.

Fixed

• Switching demos refreshes every view — picking a different trace in the viewer's dropdown now
  re-renders the active tab against the new trace and hides tabs the new trace doesn't populate.
  Previously a pane could keep stale content from the previously-selected trace — e.g. the Goals tab
  still showing the last trace's goal.

v1.3.0

Added

• OpenTelemetry bridge — ponens otel import <otlp.json> converts an OTLP-JSON span export into a
  ponens trace: spans → actions, parent-span tree → meta-actions, span start/end → action timestamps,
  and the ponens.inputs/outputs attribute convention → artifact lineage.
• Langfuse bridge — ponens langfuse import <trace.json> does the same for a Langfuse trace export
  (nested SPAN / GENERATION / EVENT observations).
• ponens demos — list and get bundled, checkable sample traces that ship with the CLI.
• Machine-readable checks — ponens trace check --json emits the policy_evaluations array;
  --write stamps it back into the trace file (self-describing traces).
• Policy evidence — evaluations now carry evidence_action_ids / violating_action_ids (plus the
  matching artifact ids); the visualizer renders these on each policy card.
• Data-driven high-stakes surface — the high_stakes_path predicate reads trace.high_stakes_paths
  (falling back to the demo defaults), so "where formal methods make sense" is decided by evidence.
• Policy packs — "Apply Formal Methods Where It Makes Sense", and the "Agentic Execution Provenance"
  spec mapping the FIX AI Working Group's six discussion points onto the trace model (with worked
  pass/fail example traces under examples/fix_ai_wg/).

Fixed

• make release reads the version from pyproject.toml (no longer depends on uv version --short).
• pyproject.toml uses an SPDX license = "MIT" expression, removing the setuptools ≥77 deprecation
  warning on upload.

v1.2.2

What's Changed

• add release Make recipes by @hon-gyu in #1

New Contributors

• @hon-gyu made their first contribution in #1

Full Changelog: v1.0.0...v1.2.2

v1.0.0

Full Changelog: https://github.com/imandra-ai/ponens/commits/v1.0.0