ponens

What's new

Everything new in ponens — currently v1.21.0. Update any time with pip install -U ponens.

v1.21.0

2026-10-08
Added
  • Requirement reason codes: reason_code on requirements and their rows (RECORD_OVERVIEW, "Reason codes"), a closed set that only grows - symbol_not_found, not_declared, no_evidence, worded_otherwise, unranked, weaker_than_required, in_progress, reading_not_chosen, failed, contested, out_of_date, freshness_unknown, model_revised - null exactly when the requirement is met. overview.REASON_CODES lists them; a test holds the spec's table to it.

v1.20.0

2026-10-08
Added
  • Trace Spec 1.15 (spec/TRACE_SPEC_v1_15.md, additive): - residual targets symbol (target_id the declaration, path its file), file and subject (subject_kind free text - a protocol is a subject of that kind, never a target type); a residual's own residual_id; - verification status bounded - holds within the bounds stated on the result (bounds), e.g. a TLC or Apalache check within bounds. Never a proof: inconclusive for a criterion, and proved does not match it; - goal status superseded with superseded_by; a goal's ticket; a criterion's stable key; - witnessed_by on a VerificationResult and a FormalModel (who ran the reasoner and recorded its answer), with a result's model_checksum, verification_id, formula, job_ref, and a model's declarations and engine; a VerificationGoal's statement and within_subject; - model inputs (§10.13): a SourceCode, Documentation or UserInstruction artifact that is a model's input, read and fingerprinted at a commit (input_id, kind, grain, checksum, read_at, why, …); - payloads for SearchResults (query, scope, commit, matches, hits) and Plan (approach, intended files); - a ConformanceResult's command, passed, failed and interface check; a region's invariant_checked, sample and sample_output; an EditFile's created.
  • The trace wire schema, as JSON Schema - ponens/schema/trace.v1_15.json (draft 2020-12; trace.v1_14.json, the 1.14 projection, shipped beside it unchanged), shipped in the package and printed by ponens trace schema (--path for where it is). It is the interchange projection of Trace Spec 1.15 (§16) as ponens reads and writes it: the envelope, actions, meta-actions, goals in both forms, and a typed payload for every known artifact type, with the closed vocabularies in their wire spelling. Extra fields are allowed; tools/strict_schema.py derives a variant that lists them. Generated by tools/build_trace_schema.py; tools/calibrate_trace_schema.py runs it over real traces.
  • ponens trace validate checks the wire schema when jsonschema is installed (pip install ponens[schema]), reporting each violation as an error under one rule; without it the check is skipped and said so, never passed. --no-schema skips it. Every trace ponens ships validates.
Changed
  • A bounded check is bounded, not sat: CodeLogician's verified_upto verdict is reported as bounded (strength unchanged, sat); sat keeps its meaning - a satisfying instance was found. Proved goals with bounded ones fold to bounded.
  • TRACE_SPEC_VERSION is 1.15; ponens version reports it.
Fixed
  • trace merge --combine writes result_id on a CarriedForward (§15.3 requires it), and via_assumptions for an uninterpreted-opaque carry - a reader no longer infers which result was carried from derived_from.

v1.19.0

2026-10-07
Fixed
  • F and G under another operator look forward from the current action, as the policy language defines them (POLICY_LANGUAGE §2.8: (τ, i) ⊨ F φ iff some j ≥ i), and as the browser evaluator and the formal model already read them. ponens trace check read a nested F as "anywhere in the trace", so G(EditFile → F(RunTests)) passed on tests run before the edit, and on an edit with no test after it so long as one ran after an earlier edit; a nested G likewise looked back. Top-level F φ and G φ are unchanged. Policies whose verdict this changes: those with F or G inside G(… → …) - "after the edit" now means after it.
  • The IML compiler emits finally_from / globally_from (defined in the generated file) for a nested F / G.
  • Parity corpus: cases for F and G under G, which the two evaluators had disagreed on unseen.

v1.18.0

2026-10-05
Added
  • Exact criteria. A typed criterion may carry statement: it is met only by evidence whose payload reports that very statement (whitespace aside, case kept) - never by words, never by a substring ("P" is part of "P -> Q"). A producer puts the statement on a result only when its checker accepted the result as proving exactly it.
  • property_match: "exact" on a criterion: its property must be one the evidence states, case and spacing aside - not a substring, which lets a weaker claim ("never negative unless refunded") answer a stronger criterion ("never negative"). Evidence worded alike becomes candidates (artifact and its wording) on the item and on the overview's requirement, whose reason says a person decides. The criterion's own subject named in front is the same words - "fee_for is never negative" meets "never negative" of fee_for; a qualifier never is.
  • linked_evidence on a criterion: artifacts a person linked to it answer it whatever their wording - still of the required type, about the component, and judged by their own verdict.
Unchanged
  • Criteria without statement or property_match match by substring, as before: records already written read the same.

v1.17.2

2026-10-04
Fixed
  • A merge no longer carries a result about a subject forward as untouched when its model changed. A result whose target is not one definition of the model - a subject: a service, a module, a protocol - had an empty closure, fell back to its bare name, and that name is in no delta: it was always carried, falsely fresh. Its closure is now the model's: the closures of the model symbols its goal maps it to (model_symbols on its VerificationGoal), else every definition of the model. A result about a definition is unchanged.
  • The legacy freshness heuristic reads a Diff's target_symbol, not words in its name. An edit to refund_fee in src/refunds/fees.py made a result about refunds (or fees) stale because the word appeared in the path. A Diff that says which declaration it changed now names that one only; a change naming no declaration keeps the conservative match on its name.

v1.17.1

2026-09-30
Fixed
  • Evidence no longer goes stale when more model is admitted after it. A definition's text ran on to the next top-level let, so a comment above the next definition, the blank lines between them, or a verify/type after it counted as part of it: a session that admitted anything more (a contract, a lemma) made every earlier proof and decomposition read as stale. Definitions now end at the next top-level item, and the checksum ignores comments and formatting - as TRACE_SPEC §10.4a already required.
  • A change to a type now makes what uses it stale. type declarations were never part of a definition's dependency closure: adding a constructor under a function left its proofs fresh.
  • Results from CodeLogicianOracle could never read as fresh. It stamped the runner's hash of the whole model text as task_checksum, which freshness compares with the closure checksum. It now stamps the closure checksum of the symbol it verified; a stored checksum that is not a closure checksum is set aside and the closure recomputed.
  • Reproducibility no longer counts a commit as a command to re-run. GitCommit was in the denominator of replayable actions, though a commit is reproduced by binding the trace to it (the axis's other term) and git commit is never replayed - so any trace that committed fell short of full marks however much it recorded.
  • A command the replayer will not run counts half. The axis counted any recorded command in full while trace reproduce replayed none of them ("2 reproducible command(s); 0 safe to replay"); its note now says how many are safe to replay.
  • JavaScript and TypeScript test runners replay. node --test, vitest, jest, npm run test, pnpm test, yarn test, bun test and deno test join pytest, go test and cargo test as safe to replay.
  • Region-test runs count as test runs. A ConformanceCheck (the model's region tests run against the code) is re-runnable like RunTests; a record whose only tests were its region tests scored as having nothing to re-run. A command on any other step is no longer counted toward the runs.
  • More runners replay: python -m unittest, mvn test, gradle test / ./gradlew test, dotnet test, swift test.
  • The flagship sample says how it is re-run. stripe_v1_1.json records the command of its test run and what of it is reproducible; it stays unbound - its source is illustrative, not in a repository. Reproducibility 30% to 75%, grade B (84) to A (92).

v1.17.0

2026-09-29
Added
  • ponens push signs in. PONENS_HUB_TOKEN is sent to the hub as Authorization: Bearer (WARRANT_URL and WARRANT_TOKEN are read too, so one pair of settings serves Imandra Warrant's agent integrations and the CLI). A refusal (401) says which setting to fix; the token is never printed. A hub that requires sign-in refused every push before.
Fixed
  • A push the hub already holds is said as such. When the hub keeps a push as a pointer to the record that already holds the same work (duplicate_of), ponens push reports that record and remembers its id - it printed the pointer as a new record before.
Changed
  • named_by_goal counts subjects. An edit is named by the goal when every symbol and every subject it says it changed is some criterion's component - so an edit to package.json whose Diff states subject: {kind: "dependency", name: "left-pad"} is named by a criterion about {"dependency": "left-pad"}, with no file criterion needed. A subject is read only where it is stated (payload.subject or payload.subjects), never guessed from other payload fields; an edit that names neither a symbol nor a subject still needs its file named.
  • A criterion about a subject is met by an artifact stating that subject in full (payload.subject: {kind, name}), as well as by payload.<kind>.

v1.16.1

2026-09-28
Added
  • Criteria about a file or a named subject. component may name a file (a path or a glob) or any subject - endpoint, table, config, dependency, module - as well as a function. "The migration is tested" or "the endpoint still conforms" was not a typed criterion at all before, and read as "no evidence yet" with the evidence in the record.
  • named_by_goal and the criteria collection understand files and subjects. An edit is named when every file it changes is named by a file criterion (a path or a glob) - a migration has no symbols to name. Each criterion in ∀ c ∈ criteria gains file, subject and about (whichever names it), so "every criterion says what it is about" is c.about ≠ ∅ rather than a rule only function criteria pass.
  • trace next says CONNECT when the answer may already be in the record. A criterion with no evidence, where the record holds a result of the required type that roots in nothing the criterion names, now gets a connect step naming those results - a decision to take (is this the answer? then link it), not "go and produce it again". Only the required type counts, and only for criteria that name a component. On a 73-record corpus, 16 records that were told to redo finished work now say CONNECT.
  • trace overview says the two things its silence could not. "No definition of done" when a goal states no requirements (it used to look exactly like a clean run), and "recorded but unconnected" when a goal's criteria are answered by none of the verdicts in the record. Reported, never scored.
  • ponens version --json: which trace spec this ponens reads. A consumer (a hub, a CI gate) can now refuse to judge a record written for a newer spec, whose new fields this ponens cannot see, instead of reading its silence as a pass. Prints {"version": …, "trace_spec": "1.14"}; --version is unchanged.
  • One table of typed-criteria use cases (tests/unit/test_typed_criteria_matrix.py, 31 rows): proofs, decompositions, tests, a person's review, conformance, files, subjects, searches, observations, project-level criteria - each held to the state trace overview should give.
Fixed
  • A property narrows evidence that says what it checked - not only proofs. Narrowing had been limited to verdict types, so a test run of "stays within the ceiling" satisfied "is never negative". Evidence that names a property is now judged by it; evidence that names none (a decomposition, a diff) still answers any property of its subject.
  • A goal whose criterion asks for a decomposition resolves. Decomposition criteria with a property never resolved, because the narrowing demanded a property a decomposition cannot state.
  • A rejected review is not a met review. rejected, changes_requested and denied are evidence against; approved and accepted establish. An unrecognized status had counted as "a review exists".
  • A search nobody could reproduce establishes nothing. Evidence with confirmed: false is inconclusive, not met.
  • next and goal coverage read components the way resolution does, including files and subjects, and compare evidence types across spellings (Decomposition / StateSpaceAnalysisResult).

v1.16.0

2026-09-28
Added
  • Goals and provenance in the policy language. A policy can require that every change serves a declared goal: ∀ c ∈ criteria . … quantifies over every acceptance criterion of every goal (with symbol, evidence, required, author, intent_author); new action predicates goal_declared, named_by_goal (every symbol an edit changes is some criterion's component), signature_change and search_confirmed (facts stamped on a Diff / SearchResults by whoever computed them). So "every changed symbol is named by a goal" or "a signature change is preceded by a confirmed caller search" is a policy, not hub code.
  • labeled(<name>): an organization's own vocabulary in a formula. A record's path_labels ({"migrations": ["db/migrations/**"]}) names parts of the code; labeled(migrations) holds for an action that changed a file in one. A pattern with a wildcard is a glob, one without a path fragment. So "a migration is preceded by tests" is written once, and each repository says where its migrations are. An undefined label holds nowhere, and the policy reads as not applicable.
  • Goal coverage. The work recorded under a goal, against the work that evidences it: goal_coverage(goal, trace) reports recorded / rooted / unrooted artifacts per goal (with a breakdown by type, and the criteria nothing answers); enrich attaches it as coverage and trace goal ls renders it. A report, not a score: unrooted work is normal, and a criterion with nothing rooted in it reads as unknown, not unmet.
  • check --json says when a pass was vacuous. Each passed policy carries applicable: false when the situation it governs never occurred (G(φ → ψ) where φ never held, a quantifier over an empty collection). The human output marks it (n/a: its trigger never occurred). A policy that passes on every record because it never applies protects nothing, and now reads that way.
Fixed
  • A goal's policies.packs resolves the pack you named. The resolver looked each pack name up as a policy SOURCE, so a real pack id (apply-formal-methods) matched no source and expanded to nothing - silently: the goal read as having no governance at all, and the Goal Contract's own example (apply_formal_methods) never governed anything. A pack is now the set of policies whose pack is that id, across configured sources; source/pack qualifies it, snake_case names the same pack as kebab-case, and a pack in more than one source must be qualified. The resolution tests had pinned the old behaviour by mocking get_source to accept any name; they now exercise real pack membership.
  • A policy or pack ref that does not resolve is reported, not dropped. Enrich records it on the goal as governance_unresolved (ref, kind, reason) and the goal is not governed - governance the author declared but that could not be evaluated is not governance. check --strict fails on it.
  • check gates goals even when the record carries no trace-level policies. It returned "No policies to check." before looking at goals, so --strict passed a goal whose governed axis failed whenever the record itself attached no policy - the documented gate did not run.
  • Local policy sources' packs resolve. Catalog entries built from a local source dropped each policy's pack, so its packs could be listed but not used.
  • check --json reports each policy's name and severity. Whether a failure blocks depends on its severity, and a consumer had to re-resolve every policy to find out; goal governance evaluations already carried both. The evaluations --write stamps into the record are unchanged, as Policy Spec §7.1 defines them.
  • The agent guide names the pack as the gallery does (apply-formal-methods).

v1.15.5

2026-09-26
Fixed
  • push now sends the trace, not just a row about it. POST /traces/{id}/content was served from the beginning and nothing ever called it, so a pushed trace arrived as a title, a commit and a content hash with nothing behind them - the viewer had no artifacts to render, the goal and gap summary had nothing to count, and a policy run over the record had no record. Nothing failed: push reported success, and the hub showed a trace whose every number was zero. The summary field sent alongside was trace.get("summary"), and a ponens trace has no top-level summary, so that was always None too; a hub is better served deriving it from the content it now receives. Two tests assert the upload happens and that it follows the create call whose id addresses it.

v1.15.4

2026-09-25
Added
  • Replays can decide whether a verdict still holds. A record now carries its own check. trace reproduce --run compared by substring before - the record's verdict word against the engine's raw output - and measured against a live ImandraX run that can never match: none of proved, refuted, unknown or bounded appears anywhere in it. Every replay reported DIVERGED on a verdict that had reproduced exactly, in the alarming direction, on the one path a person takes to verify. expected_output.check names a JSON path and what must be there, which keeps ponens engine-agnostic - a path needs no knowledge of ImandraX, or Lean, or a test runner. Records without one keep the old comparison.
  • trace goal resolve <goal> --take ours|theirs - settle a goal the merge found contested. Choosing is an amendment like any other, so the version not taken stays in the record rather than disappearing behind the one that won, and the residual is marked addressed with who decided and why.
  • Merge reports goal divergence. trace merge --combine deep-copied ours and overlaid only model artifacts, so a branch that TIGHTENED a goal - broadened the intent, added a required criterion - had the tightening silently discarded, and a goal the other branch introduced vanished. No residual, no report line: the totality invariant covers result_id only. A field one side moved is now taken; a field BOTH sides moved differently is a conflict the merge refuses to settle, recording both readings and opening a goal_divergence residual. A goal states what the work is for, and that is not an algorithm's call.
Changed
  • A goal whose definition is contested is never met, and never certified. Every criterion may resolve to done - but under which definition of done? Nobody has said. Kept in step across the Python, the viewer and the parity corpus.
  • The grade's Reproducibility axis counts commands, not objects. It counted any action carrying a reproducibility block, while the replayer reads procedure.command, so one trace scored 100% and "4 replayable action(s)" while trace reproduce on the same file found none. Grading a record on an auditability nobody can exercise is the failure that axis exists to detect.
Fixed
  • A criterion can name the property it is about. Two criteria over one function were the same criterion to the resolver - "clamp stays within its bounds" and "clamp swaps inverted bounds" both matched the first verdict for the component, and the one that had been proved came out blocked.

v1.15.3

2026-09-22
Added
  • Every validation error now states the rule it breaks, and cites the spec. trace validate named the violation and never the rule. "action 1 is in two meta-actions (m1 and t1)" is a statement about your data; it is not a statement that nesting is expressed with parent_id rather than by containment, which is the belief you actually hold wrongly - so an author who built a deliberate parent/child structure reads it as a description of what they built and looks elsewhere. That cost a producer a day of invalid records. Errors breaking the same rule are now grouped and the rule is stated once, with the section of TRACE_SPEC that says it; --all lists every error rather than summarising the ones that break a rule already shown. Closed-vocabulary errors spell out what was permitted, and cite the section defining that vocabulary rather than a general one.
  • policies remove <id> --from <trace> - the counterpart to policies add --into. Attaching was possible and detaching was not, so a rule picked up by mistake could only be taken out by hand-editing the record.
  • policies attached <trace> - what rules is this record actually being judged against? search says what exists and check gives the verdict; nothing said what a given record carries. With nothing attached it says so plainly, because no policies attached and every policy passing produce the same silence in every downstream summary, and only one of them means anything was checked.
Changed
  • Reading an invalid trace says so. validate and check refused one; every other command reported on it and exited 0 - overview printed a gate verdict, status a summary, residuals a gap list - none mentioning that the record underneath had been rejected. A reader got a confident report about a record nothing downstream would accept. It is a warning rather than a refusal, because diagnosing a broken record is exactly when you want to read it; set PONENS_NO_VALIDITY_WARNING=1 to silence it.
  • trace check says that nothing was evaluated. Policy evaluation validates before it evaluates, so an invalid trace means no policy ran at all - an absence that otherwise reads as a pass.

v1.15.1

2026-09-21
Added
  • A gap the record already answered is marked overtaken. An engine unknown has two ways out - prove it, or accept it with a justification - and a third happens constantly: the property is proved on a second attempt and the gap sits open beside the proof that answers it. classify_undecided now matches a later proved result back to the gap, by the goal's description rather than its target symbol. The symbol is derived from the goal text and the same property appears under different symbols; worse, a weaker property about the same function would have matched and retired a gap nothing had answered. A property reformulated to get it through - bounded, or with a strengthened hypothesis - has a different description, retires nothing, and that is correct: a proof of a different statement did not establish this one.
  • ponens trace residual marks retirement without closing anything. overtaken carries why, recheck and by, and status stays open. A bounded proof also reads proved on the wire, so this is a reason to look again, never a claim that the property holds unconditionally.
  • cli/tools/ponens-live.py serves trace view and redraws it whenever the trace changes. It shells out to the real viewer on every rebuild rather than reimplementing any of it, so a change to the viewer needs no change here.
Changed
  • trace overview stops repeating itself. A standing assumption that every record carries is collapsed to one line rather than restated per artifact; gaps that share a cause fold together; and abandoned work - a property attempted many ways where only the first attempt carried derived_from - is reported as one item rather than counted once per attempt.
  • trace next says something true when no requirements were declared, instead of advising work against a goal that does not exist.
Fixed
  • The reloader in the live viewer is injected at the last </body>. The viewer's print function builds a page inside a template literal, so the file carries the tag twice; injecting at the first one put a <script> block inside a JavaScript string, whose </script> closed the viewer's own script tag early and spilled the rest of viewer.js onto the page as text.

v1.15.0

2026-09-20
Added
  • A gap is closed by appending the decision, not by editing the gap. ponens trace residual resolve <trace> <id> --status acknowledged|addressed|waived --justification "…" [--evidence <artifact>] [--by …] writes two things - a Decision action carrying the justification as its rationale, and a ResidualResolution artifact (spec §13.3a) hanging off the residual in the lineage DAG - and leaves the residual exactly as its producer declared it. Editing status in place is indistinguishable from never having declared the gap: the record loses who decided, on what grounds, against what evidence and at which point in the work, and a reader cannot tell a reasoned waiver from a quiet deletion.
  • A justification can be invalidated without being removed. ponens trace residual contest <trace> <resolution id> --reason "…" [--defeater-kind rebuts|undermines|undercuts] [--by …] declares a defeater residual against the grounds for a closure. A justification is a claim, and this model attacks a claim with a defeater rather than a deletion - so while that defeater is open the resolution is not in force and the gap reads open again, with both the waiver and the reason it does not hold still in the record. Withdrawing the objection is the same move in reverse: resolve the defeater and the closure stands again, the whole exchange readable.
  • Every declared gap names the step that surfaced it. ponens trace residual add takes --introduced-by <action id>. It is written to both carriers a consumer might read - payload.introduced_by_action_id and the artifact's producer_action_id - and validated against the trace: naming an action that does not exist is rejected with nothing written, because a live link to a step that isn't there is worse than no link. Omitting it is still legal and now says what it costs. Never inferred from the most recent action: attributing a gap to the wrong step would be worse than leaving it open.
  • cli/tools/check_demo_provenance.py — a release check over every shipped trace: each residual names an introducing action, the two carriers agree, the action is in the trace, and every derived_from, target and related edge resolves. Runs in validate-samples. Validity and provenance are different questions, which is why this sits beside check_demo_spec.py rather than in the validator.
Changed
  • The viewer answers "where did this come from" on the card. Each residual reads surfaced by #22 Verify: all 7 amount invariants - PROVED · about updated_iml_model a8, with the step as a link that jumps into the flow and scrolls it into view; artifact ids resolve to the names their authors gave them. A residual with no introducing step renders surfaced by: not recorded.
  • Every reference on a residual card is now a link. The card itself opens the residual in Artifacts - a residual is an artifact (§13), and the card was a dead end that led only to the step that surfaced it - and the artifacts it is about and related to select there too. Both places that show a residual in detail gained the same Surfaced by: the graph's side panel, which returned before the generic panel's Producer and so showed nothing about origin while every other artifact showed it, and the standalone overlay, which showed a bare Introduced at step #22.
  • Every shipped example is attributed. Each demo residual now names the step at which the gap actually becomes visible - the coverage gap in the Stripe trace attaches to the decomposition that exposed which transitions carry no goal, not to whichever step came last.
  • AGENT_PROMPT.md and the embedded agent prompt tell agents to pass --introduced-by, and how to choose the step: the one where the gap became visible, not the one they happen to be on.
  • Amending the definition of done is an append too - and it was the sharper hole. A waived gap still reads as a gap; a withdrawn acceptance criterion left nothing behind at all. ponens trace goal drop was acc.remove(item): deleting the single unmet criterion from the shipped Stripe demo moved it from 88% to 100%, and ponens trace integrity reported nothing lost, because it indexed only criteria that were already done. goal drop / goal rm / goal set (when replacing) now require --reason and append a GoalAmendment (spec §18.3a) carrying the criterion verbatim, the reason, the author and the step. goal certify appends too - a second review used to overwrite the first, so a changes-requested verdict could be replaced by approved with nothing to show for it. trace resolve and goal ls print ! the definition of done was amended N time(s) next to the percentage, because a percentage only means something against a fixed bar.
  • ponens trace integrity indexes every acceptance criterion, not only the met ones - so a withdrawal is reported as a loss whatever state the criterion was in, rather than only when it had already been achieved.
  • The agent's own store keeps what the trace cannot recover. The register above was built from ponens' file-mutation surface, which is the wrong frame for an agent: CodeLogician regenerates its trace from .codelogician/ state on every export rather than appending to a file, so append-only rules reach nothing the store overwrites - anything the store forgets is gone before the record is written. Three places it forgot: a second decision about a residual overwrote the first in the store, so a waiver later superseded never reached the trace at all; re-declaring a goal with fewer criteria dropped them silently (the agent-side form of narrowing the bar); and the desktop's "Clear goal" wiped the definition of done with nothing left behind. The store now keeps a decision history per residual and a list of goal amendments carrying each dropped criterion verbatim, and the exporter emits them as ResidualResolution / GoalAmendment records. A store written before this still loads.
  • Workflow stories, asserted on what a person reads. Thirteen end-to-end runs through the CLI in the order someone actually works (test_user_stories.py), plus the agent/ponens handoff (handoff.story.test.ts): a refuted property fixed and re-proved; a gap waived, contested, and settled; a criterion withdrawn before a release; handing a finished record to someone who was not there; and the gate speaking plainly. They assert the OUTPUT, not the structure - which is the class the property suites cannot reach, and the class several real bugs fell into (check printing -2 advisory, overview reporting "no policies attached" on a trace carrying eight, grade calling a warning a failed gate). Writing them turned one up immediately: trace next said "no open gap has a suggested check" while trace residuals listed exactly such a gap on the same record - a standing assumption is deliberately held back from the to-do list, but the message denied it existed. next now names standing assumptions as the boundary the evidence rests on rather than claiming there are none.
  • ponens trace next never reported stale evidence. Its refresh branch read only evidence_ref, which enrich populates for a TYPED criterion; for an untyped one - which is what ponens trace goal accept creates - the resolved id goes in evidence instead. So no criterion authored through the CLI could ever produce a refresh step, and "re-run the affected result", the promise the whole freshness machinery exists to keep, was never once made to anyone by the command whose job is to say what to do next. This was the THIRD bug in this one function from evidence carrying two shapes (after the crash and the art label above), so it is now read through a single _resolved_evidence_ref accessor rather than fixed a third time in place.
  • Stale evidence that no acceptance criterion covered was invisible to ponens trace next. The refresh branch fires only through a goal item, and the gap loop deliberately skips derived residuals, so evidence that went out of date on a record with no goal fell between them: trace residuals --derived said "out of date, re-run it" while trace next said "nothing to do". A merged record is the ordinary way to land there - trace merge --combine carries the evidence and declares no goals. next now reports uncovered stale evidence in its own right, without double-reporting it when a criterion does cover it.
  • Evidence that says no no longer satisfies a criterion. Three binding stories - a claim that code implements a published spec, the catalogue publishing a new version underneath it, and the binding being removed - turned up the worst kind of defect this format can have: a failed conformance check resolved its criterion as done. trace resolve read 100% ✓, goal ls read MET, trace next read "Nothing to do", and there was nowhere a reader could find out the evidence said the code does not conform.
  • The agent's record is now read by real ponens in CI, not just validated by it. export-validity.test.ts proved the export is well-formed; well-formed is not understood. The handoff story hands a record the agent actually produced - a gap closed twice, a criterion dropped by a re-declare - to the installed ponens and asserts it answers the questions a person asks: the gap reads closed with both justifications and the superseded one marked, the withdrawn criterion says it was not met, and every reader runs without crashing.
  • Checks that generate checks, rather than one more assertion someone thought to write. Every hole in this release was found by a different kind of check - reading a demo, following a click, sweeping commands over fixtures, a round-trip, enumerating state transitions - and each kind found a class the others could not. Two checks now cover the classes rather than the instances: - Record invariants (test_record_invariants.py) compose the operations an agent can actually perform at random and assert what must hold regardless: nothing ever declared becomes unreadable; the record's apparent standing improves only by adding evidence or by a recorded decision; every reader still runs; writing and re-reading changes nothing. Seeds print on failure so a counterexample replays exactly. Verified by regressing goal drop to its silent removal - caught in two steps, goal accept -> goal drop. - Three-way derivation parity. Whether a gap is open is decided in Python (ponens trace check), JavaScript (the viewer) and TypeScript (the agent). They were kept in step by writing the same rule carefully three times, which is not a mechanism: a viewer showing a gap as open while check passes it is worse than either alone, because neither side can see the disagreement. One fixture corpus, one expected answer generated by ponens, all three asserted against it (viewer/parity.test.mjs in CI, derivation-parity.test.ts in the agent).
  • A register of every state transition a trace holds (cli/ponens/transitions.py), classifying each as derived (computed on read - nothing to forge), appended (a decision that is itself a record), or applied (written in place, each with the reason that is tolerable). trace residual resolve and the goal amendments above are the two rows that moved from applied to appended; they were found by writing the register. Gated in both directions: a new state type in the published spec fails until it has a row, a row whose states drift from the spec fails, an applied row with no justification fails, and the set of commands that let a status be asserted is pinned - so an earned verdict cannot quietly become a declared one.
  • Trace spec 1.14 (spec/TRACE_SPEC_v1_14.md) - additive, backward-compatible: §13.3a defines the ResidualResolution artifact and derived residual status. Traces from 1.4 onward stay valid and unchanged, and editing status in place remains readable; it is simply no longer how the CLI closes a gap. Shipped demos re-stamped to 1.14, and sample_auth_xstate now carries a real waiver so the mechanism is visible on the demo page beside a gap closed the old way.
  • The viewer shows how a gap was closed - status, who, when, the deciding step (clickable) and the cited evidence - on the residual card and in the Artifacts panel, with superseded decisions dimmed rather than hidden. It derives status exactly as the CLI does, so the two cannot disagree about what is open.
Fixed
  • ponens trace next crashed on an acceptance item whose evidence is a plain artifact id. evidence carries two shapes - the requirement ({"artifact": "VerificationResult"}) on a typed criterion, a resolved artifact id on an untyped one, which is what enrich itself writes when there is no requirement object to preserve. next read the second as the first and raised AttributeError: 'str' object has no attribute 'get', taking the command down on the shipped Stripe demo among others: the one command whose job is to say what to do about an open gap.
  • Provenance recorded in the standard place was thrown away on render. Projecting a Residual artifact back to the residual surface read only payload.introduced_by_action_id and ignored the artifact's own producer_action_id — the field every artifact is required to carry. A trace that recorded the introducing action the ordinary way displayed as though it had none.

v1.14.0

2026-09-18
Added
  • ponens trace symbols <trace> — the index. Takes an optional --file <requirements>. One small record per symbol the trace knows anything about: the symbol, its file, what backs it (decomposition · verification · conformance · model · tests), its grade, its freshness, how many regions and open gaps, the requirement it serves, and the entry to cite. About 25 tokens each, so a project fits in a prompt. Deliberately enough to decide whether to ask a second question and never enough to answer one. Latest entry wins per symbol — history is in the trace and is not what an index is for.
  • ponens trace symbol <trace> <symbol> — the detail. Summary by default: the evidence with grades and freshness, the open gaps worst-first, and shape — which variables the behaviour actually turns on and how many distinct outcomes there are. Two lines that answer most questions without returning a single region.
  • --regions, with --where and --limit. The region map itself, each case as the constraints that reach it and the result it produces. --where takes a substring over constraints and results, or outcome:<label> · diverged · raised. On a real 83-region decomposition this is the difference between a page and three lines.
  • spec/RECORD_QUERY_v0_1.md — the companion that fixes the shapes, the size budgets and what must always be said. Sits beside RECORD_OVERVIEW_v0_1.md: that one answers where a project stands, this one answers what is known about a symbol.
Changed
  • Size is part of the contract, not left to the caller. An interface that returns everything defeats the purpose of asking rather than reading. The index is one line a symbol; the detail is a summary until regions are requested; a region list is capped and a truncated answer always reports what it left out.
  • Every answer carries its freshness, never as a separate call. Substituting a stored result for reading the source is only safe if a stale answer says so, and a consumer may trust fresh, must warn on out_of_date, and must not treat unknown as either.
  • A region map says whether it is exhaustive. complete, with a bound when recursion forced a depth. "Every case satisfies it" and "every case to depth 12 satisfies it" are different claims, and a consumer that cannot see which it has will conflate them.
  • Absence is an answer. An unreasoned symbol returns {"known": false} rather than an error. Nothing is inferred, and no gap is filled with something plausible — the caller should read the source.
  • Gate: says whether anything was asked. ponens trace overview printed a bare Gate: pass for a trace with no policies attached, which reads as an endorsement of the record rather than a statement about policies — a record carrying a refuted property and a failing test suite still said pass. The state is unchanged and remains correct (no policy blocked anything, because none was evaluated); the rendered line now carries the context the data already held: Gate: pass (no policies attached - nothing was checked), or (3 rules checked) when rules did run. Found by querying a trace rather than by reading one.

v1.13.0

2026-09-12
Added
  • ponens trace overview — where the record stands, in five words (spec/RECORD_OVERVIEW_v0_1.md). One JSON for every screen: requirements (from a requirements file — the agent's bindings.yaml — and from every goal item not derived from it), gaps by state (missing · assumed · failed · out of date), the gate (pass · blocked by …), next steps (fix · meet · refresh · gap · optional), evidence per symbol graded (proved · witnessed · tested · checked · attested), record health. A read over enrich, next_steps, stale_evidence and blame; no renderer re-derives semantics. ponens trace requirements <trace> --file <bindings.yaml|.json> is the requirements part alone: one row per requirement and per named symbol, joined from the file, the trace's goals, reference artifacts, conformance results and the reasoner freshness, with the seven row rules and the model's revision / reading states. ponens trace integrity <before> <after> names the established evidence after no longer holds (a passed conformance or a proof gone, a reference no longer cited, a done item reopened; exit 3), so a save hook can refuse to weaken a record quietly.
  • PyYAML is now a required dependency (pyyaml>=6): the requirements file is YAML.
Changed
  • Derived freshness residuals speak the five words: a result is "out of date" (was "stale") and "no longer tied to its subject / its model" (was "detached"). Residual kinds (stale_evidence, detached_evidence) are unchanged.
  • ponens trace next — what the record says to do next. Folds the enriched trace into one ordered list: blocked goal items to FIX (a failed conformance, an open defeater), required items to ESTABLISH, done items whose evidence went stale to REFRESH, open residuals with a suggested_check (GAP, highest severity first; a standing assumption counts only at high/critical), then OPTIONAL items. --json for agents (CodeLogician injects it into every turn), --limit N. goals.next_steps / render_next.
  • Action: the requirements check on the pull request. New input bindings (auto | path | off) — the action runs cl requirements --json (or reads a pre-computed JSON in the trace requirements shape) and posts one row per requirement, or per code symbol → model symbol, with its evidence (grade, fresh or out of date) and state; a blocked requirements gate fails the job under fail-on. Output bindings.
  • Bindings in the record — conformance against a reference (Trace Spec 1.13, §11.2–11.3, additive). A ConformanceResult may name a reference artifact as its reference_artifact_id (a catalogue entry a repository is bound to), with the reference as a valid derived_from parent and entry_symbol / target_symbol / conformance_kind / reference_version / reference_checksum on the payload. A goal criterion may carry reference: it is then met only by evidence judged against that reference — a proof of some other property of the component no longer resolves a conformance item (enrich). Reference freshness: such evidence is stale_evidence once the trace's reference artifact carries a different version or checksum, detached_evidence when the reference is gone (stale_evidence / reference_freshness), healed by a later result. New policy predicate conforms_to(<reference id>) (an unversioned id matches any version). soundness_errors rejects a reference_artifact_id that names neither an artifact nor a reference artifact.
  • ponens trace blame — evidence per symbol (git blame for what was established). For every code symbol a trace carries evidence about: the best standing result (the strongest FRESH one; strength rank, then latest), its evidence_strength, its freshness (fresh / stale / detached / unknown, from the same derivations enrich uses, plus a producer's artifact_freshness), the oracle that produced it, a counterexample when refuted, and the open residuals anchored to it. --json for renderers (CodeLogician's cl blame gutter, a PR comment, a desktop gutter), --symbol to filter.
  • ponens bind writes a scorecard into the git note. Under the Trace-Id: line (unchanged, first), the note now carries Grade, Policies (the gate), Gaps (open, high) and Goals (met, at risk), so git log --show-notes=ponens reads as an evidence log per commit. Best-effort: a trace that cannot be graded still gets its Trace-Id.
  • GitHub Action — a checked reasoning trace on every pull request (action/). uses: imandra-ai/ponens/action@v1.13.0 finds the trace an agent published under .ponens/ (or reconstructs one from a session transcript with ponens emit), validates it, runs the policy gate (trace check over the trace's policies plus gallery policies: / a local policy-file:), resolves the goals (trace enrich: met, weakest-link strength, at risk, open gaps) and posts the trace report scorecard as a job summary and as ONE pull-request comment updated in place. A failed error-severity policy fails the job (fail-on: error | warning | never), so the check can be made required. Runs entirely inside the workflow's runner; the repository file is never modified. The repository dogfoods it (action-selftest.yml).

v1.12.0

2026-09-11
Added
  • Oracles are a generic type (ORACLE_SPEC_v0_2, Trace Spec 1.12). An oracle is fixed by its contract, not its mechanism: a formal reasoner, a test runner, a static analyzer, a database or reference-data store, an LLM judge and a human sign-off are all oracles on equal footing. The oracle_type set is declared open (standard names are a classification; consumers warn on, never reject, an unknown name) and monitor joins the standard set. Every evidence payload MAY carry an attribution block payload.oracle (id, type, version, and the honest strength of this result). The reasoner-only reasoning_fingerprint is generalized to an evidence fingerprint (subject_checksum / subject_ref / valid_until), so derived freshness is defined for any oracle's evidence and gains an Unknown outcome; an optional probe operation re-reads a subject's fingerprint without re-running the oracle. A new Observation artifact (§10.11) is the typed landing place for a monitor's evidence. Policies gain strength_at_least / oracle_type / produced_by; goal resolution reports the weakest-link strength; merge prefers the stronger result.
  • Reference oracles across the spectrum. ReferenceDataOracle — a database as an oracle: a mapping or a SQLite store (from_sqlite; PONENS_REFERENCE_DB registers one as reference-data) answering a query with an Observation, graded attested, fingerprinted on (source, query, value, as-of) and probe-able so it goes stale when the source republishes and detached when the subject is gone. Plus SubprocessTesterOracle (exit status is the verdict → tests), CallableJudgeOracle (attested) and AttestorOracle (a UserApproval). ponens oracle list --type, ponens oracle probe.
  • Graded, fresh-or-not resolution. ponens trace enrich stamps each resolved item with its evidence_strength and freshness (fresh | stale | detached | unknown) and each goal with min_strength (the weakest link); any-oracle evidence with a fingerprint is checked by probing its oracle or by valid_until, and surfaces the same derived stale-/detached-evidence residuals a proof does. ponens trace validate warns on a non-standard oracle_type, errors on an invalid strength or an Observation graded above attested, and flags a strength on an unestablished result.
  • SDK. Session.verify records the action by the oracle's mechanism (Verify / Observe / Test / Analyze / Judge / Attest), with observe / test / judge / attest aliases; Session.probe and Session.freshness re-read an artifact's subject via the oracle that produced it.
Changed
  • The policy reasoner / oracle field is now enforced. Previously declarative (nothing read it at check time), it desugars into the checked formula: G(atom -> (produced_by(X) || oracle_type(X))) over every evidence-bearing atom the formula mentions (the formal-reasoning result types when it mentions none). A policy declaring reasoner: codelogician therefore fails on a trace whose proofs came from another engine or carry no attribution — a verdict that was passed before. To keep the old behaviour, remove the field; to name the engine precisely, write produced_by(...) in the formula. produced_by matches the oracle id or the engine it drives (the catalog's codelogician.engine = imandrax), so the gallery's codelogician / imandrax policies both match a CodeLogician-over-ImandraX trace, including pre-1.12 payloads that carry only engine.
  • ponens trace validate checks oracle attribution. An invalid evidence_strength, or an Observation graded above attested, is an error; a non-standard oracle_type (without specializes) and a strength stamped on an unestablished (unknown / error) result are warnings. Traces without attribution blocks are unaffected.
  • Policy formulas: an identifier may now contain - when followed by an identifier character (produced_by(calendar-db)); -> is still the arrow.

v1.11.0

2026-08-26
Added
  • Composable acceptance — the goal property language (GOAL_CONTRACT_v0_2 §9, Trace Spec 1.11 §18.1). An acceptance_item MAY now carry a formula instead of a single criterion: and / or / not / implies over atoms, plus forall / exists quantified over component selectors (glob, module, scope, tag) — so "every handler in payments/ is proved, and at least one has a conformance check" is one criterion, not a hand-maintained list. Each atom carries its own met / governed role, and resolution runs over a 4-valued status lattice rather than a boolean. A legacy single-criterion goal is exactly the atomic case and desugars unchanged.
  • Trace composition — ponens trace merge (Trace Spec 1.10 §15.3). Combines an ours and a theirs trace (optionally against a --base ancestor) and sorts every standing reasoning result into exactly one bucket, under a totality invariant: a CarriedForward artifact when the result is provably unaffected — its dependency closure is disjoint from the merge's change set, or every touched dependency was assumed uninterpreted — or a NeedsRereasoning residual when its closure or an assumed contract was disturbed. A CoverageRegression residual records a goal whose scope gained an unproven member. The merged trace records two-parent merge_event provenance; --combine emits that trace, the default emits a report projection and mutates neither input. The implementation is the sound-but-conservative realization of the proved IML model in formal/ — anything not provably safe collapses onto re-reasoning, so a stale result is never reported fresh.
  • Durable component identity — component_id (Trace Spec 1.10 §7.1). A code component keeps its identity across a rename or a move, so evidence-to-code binding — rooting, freshness, and the merge change set — survives refactoring instead of silently detaching. The resolver is tiered (producer-declared lineage → unique exact fingerprint → confident unique similarity) and never guesses: an ambiguous or weak signal mints a new id, because conflating two distinct components is the unsound error.
  • Oracles — ponens oracle list / ponens oracle show (ORACLE_SPEC_v0_1). Generalizes reasoner to oracle: anything that produces evidence about a target and returns it as trace artifacts — a formal reasoner, a test runner, a static analyzer, an LLM-judge, or a human attestor. Two orthogonal classifiers travel with the evidence: oracle_type (the mechanism — reasoner | tester | analyzer | judge | attestor) and evidence_strength (the guarantee — proof > sat > tests > static_analysis > attested), so a reviewer can see which oracle produced a claim and how strong that makes it. A reasoner is now simply the formal, proof-producing subtype.
  • ponens.sdk — instrument an agent instead of reconstructing it (SDK_SPEC_v0_1). A thin runtime SDK for agents that speak ponens natively: open a Session, record actions and artifacts as the work happens, invoke oracles for evidence, and on exit get a validated trace that passes ponens trace check — no transcript reconstruction step. It builds the same JSON-native trace the rest of the toolchain uses, so there is exactly one trace model and one code path for artifacts and lineage.
  • Integrity fields are now specified in the trace spec (1.11 §12.4, §5). content_hash and signatures — shipped in 1.9.0 and previously defined only in CLI_SYNC_MODEL / AUDIT_READINESS — are now normative in the core spec, including the HASH_EXCLUDE set, the per-signature role / disposition / RFC-3161 timestamp fields, and the uniform valid | untrusted | invalid | tampered verdict.
Changed
  • The package version jumps 1.9.1 → 1.11.0 to track the trace spec, which advanced two minor versions in one go — 1.10 (trace composition) and 1.11 (signatures + composable acceptance). There is no 1.10.0 package release; everything from both spec versions ships here. TRACE_SPEC_v1_9.md is now TRACE_SPEC_v1_11.md.
  • GOAL_CONTRACT is now v0.2 (GOAL_CONTRACT_v0_1.md → GOAL_CONTRACT_v0_2.md), and GOAL_FAITHFULNESS_v0_1 re-points at it. If you link to the spec, update the URL — the v0.1 path no longer resolves.
  • The IML / ImandraX formal models moved from spec/iml-model/ to formal/ — the framework's invariant models plus the layered trace+policy model in formal/trace-policy-model/. The merge and component-identity models there are the conformance spec the Python implementations realize.
Fixed
  • verified_claims_are_fidelity_checked no longer fires on spec-first sessions. The formula is now guarded — (F SourceCode) → G(Verify → F(ConformanceResult(passed))) — so it applies only when there is source code to conform to. An authored-IML session, where the model is the artifact rather than a translation of something, passes vacuously instead of being flagged for a missing fidelity check.
  • Trace viewer: the Steps / Actions pills now count within the active scope, so the numbers match the cards actually on screen, and each scope option's count is the actions it will really show. A detail panel can be closed (returning the flow to full width), a live same-session refresh keeps your zoom, pan, and manual DAG drags instead of resetting the layout, and the noise-only completed result line is no longer rendered on every action.

v1.9.1

2026-08-09
Fixed
  • Typed acceptance criteria now honor open defeaters (goals.py::_resolve_typed). A typed criterion (component + evidence: {artifact}) previously resolved done as soon as a matching artifact existed, ignoring counter-evidence — so a criterion whose evidence (or the provenance it derives from) is contested by an OPEN Defeater still read as met. It now resolves blocked, matching the legacy property path (§13 / §18.2). In particular a failing conformance — whose ConformanceResult carries an undermines-defeater — correctly leaves a conformance criterion unmet instead of silently done.

v1.9.0

2026-08-07
Added
  • Cryptographic sign-off (ponens trace sign / ponens trace verify) — non-repudiable, tamper-evident audit sign-off over a trace's content_hash, with pluggable backends: SSH (ssh-keygen, trusted via an allowed-signers roster), GPG (detached signatures, trusted via an allowed-fingerprints roster, with the public key inlined so verification is offline), and keyless sigstore (a short-lived Fulcio certificate binds the signature to an OIDC identity, and the proof is recorded in the Rekor public transparency log — no long-lived key to manage). An audit sign-off carries --role/--disposition; verify dispatches per signature and reports valid / untrusted / invalid / tampered, gating on failure (--require-trusted). Signatures live in signatures[], excluded from content_hash, so parties co-sign the same content with whatever backend they trust.
  • RFC-3161 trusted timestamps. trace sign --tsa <url> attaches a Time-Stamping Authority signature over the signature (a TSA-attested "existed by <time>"); trace verify --tsa-ca <cert> checks it offline against the TSA certificate — so when is attested, not machine-clock-asserted.
  • PROV interchange (ponens trace export --to prov). Export a trace to W3C PROV-JSON (Entity / Activity / Agent + wasGeneratedBy / used / wasDerivedFrom / wasAttributedTo), so the record speaks a standard provenance vocabulary auditors and tools already read (PROV_INTERCHANGE_v0_1.md).
  • Evidence freshness — Fresh / Stale / Detached (Trace Spec §18.3). A formal-reasoning result (a proof, a state-space decomposition, conformance, co-simulation) is only as current as the model it ran on. enrich / residuals --derived now derive a stale- or detached-evidence residual from a dependency-closure fingerprint of the target symbol — a change to anything the target transitively uses invalidates it, and removing the symbol detaches it — and a goal never resolves done over non-fresh evidence. Generic across result kinds, not verification-only.
  • First-class counter-evidence — Defeater residuals (Trace Spec §13 / §18.2). ponens trace residual add --kind defeater --defeater-kind rebuts|undermines|undercuts --target-id <result> records evidence against a claim (a counterexample, a model that doesn't match the code, evidence that doesn't support it). An open defeater blocks the claim it targets — a contested Property reads blocked, not done — which is stronger than a mere declared gap.
Changed
  • Freshness reasons per-symbol from the model's inline source. The check reads the model the producer already inlines (iml_code, or the spec's canonical formal_code) and selects the current model per target symbol, so a multi-file session (one focused model per formalization run) no longer false-flags an earlier symbol's proof as detached. An explicit producer reasoning_fingerprint.task_checksum on a result is honored directly; absent it, the closure checksum is reconstructed from the model current at proof time.

v1.8.0

2026-08-04
Added
  • Content-addressed object store (ponens objects) — an immutable, sha256-keyed blob store so a trace can reference large content (source, formal model, tests) by content_ref instead of inlining it: identical content is stored once (dedup) and a trace plus its reachable objects is a portable, self-contained bundle. Layout is a stable spec (<dir>/sha256/<ab>/<rest>, overridable via $PONENS_OBJECTS_DIR) so any producer that can hash may write blobs directly. New CLI: ponens objects put | get | externalize | inline | gc | stat. ponens bind --externalize moves inline blobs into the store at the share boundary; objects inline rehydrates a received bundle.
  • ponens trace replay — re-run a ReproductionBundle. Materializes the content-addressed model from the object store and re-executes it through a pluggable engine adapter (engines.py, with an ImandraX adapter), flagging where the fresh verdict diverges from the recorded one. Dry by default (reports the plan + self-containment); --run executes the safe-allowlisted replay command and preflights the engine (binary on PATH, credentials present).
  • Revision-aware lineage (supersedes / revision). Helpers for append-only revision chains: current_artifacts (fold history to the latest revision), superseded_ids, and revision_chain (walk a revision newest→oldest, cycle-safe). trace validate now warns on a dangling supersedes.
Changed
  • normalize_trace surfaces failed/aborted attempts and resolves externalized blobs. A CommandResult (carrying an outcome/exit_code) is mapped onto its action so policies can distinguish attempted-and-failed from never-attempted; externalized content_ref blobs are resolved back to inline content for policy evaluation on a bound trace.
  • Residual payload preserves summary / property / counterexample. The plain-language lead, the formal property that was checked, and a counterexample input now survive residual processing (Trace Spec v1.8 §13), instead of being dropped by the residual-surface filter.

v1.7.1

2026-07-29
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

2026-07-27
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

2026-07-25
Added
  • Goal contracts — an acceptance criterion is now a required evidence artifact over a code component: it names the component and the evidence artifact that must exist in its lineage ({ "artifact": "VerificationResult" | "Decomp" | "Tests" | "Diff" | … }). A goal also 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 (each component has its evidence artifact), 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.
  • Met and governed are cleanly separated — a criterion is met the moment its evidence artifact exists; whether that evidence was derived correctly (proved, autoformalized, tests pass, a proof required on a high-stakes path) is decided entirely by policies, the governed axis. One mechanism for rigor, no overlap. New pack policy refuted_results_must_be_reproved enforces that a verification result offered as evidence is actually proved, not left refuted.
  • 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 — evidence-artifact 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, and its summary counts goals_governed.
  • Evidence rigor moved from faithfulness grading to policy. faithfulness_of no longer emits weakly_specified (and certified no longer depends on it) — "is a diff enough, or do you need a proof?" is now a policy question on the governed axis. GOAL_FAITHFULNESS_v0_1 §6 is superseded.
Fixed
  • *Goals now reach met when the work is real — a criterion resolves by artifact lineage* (does an artifact of the required type root in this component?) instead of matching the verification goal's description text. This fixes goals that never ticked even though the evidence existed.
  • Lineage is component-precise — an artifact that declares its own target_symbol (a VG, a Decomp, a targeted Diff) is about that component, so a decomposition of one function no longer looks like it roots in every symbol the shared model formalized.

v1.5.0

2026-07-22
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

2026-07-22
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

2026-07-22
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

2026-07-22
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.x

2026-07-21
Added
  • Artifact-DAG node isolation in the visualizer — click a node to isolate its connected lineage (upstreamed to viewer/core, so the CLI ponens trace view and the VS Code plugin both get it).
Changed
  • Packaging, license, and author-metadata fixes; version alignment across the desktop wrapper.

Full history + downloads on the GitHub releases page.