Reasoning

The model is good at one question — what would demonstrate this — and disqualified from another: did this demonstration succeed. Everything in the Reasoning view is an answer to the first question.

The disqualification is not about model quality, and it does not improve as models improve. A model evaluating evidence it helped produce is biased toward confirming it, and most strongly where the code is subtly wrong — because plausible-looking evidence is exactly what a subtly wrong change produces. A judgement cannot be replayed: a deterministic program re-run over the same hashed evidence returns the same answer, while a judgement can only be asked again, and a different answer settles nothing. And the repository under test is hostile input, carrying instructions in comments, pull request bodies and fixtures; a model that both reads that text and issues verdicts is an injection target with merge rights.

So no PASS ever appears in this view. The planner's only output is a proof plan, which is validated before anything runs; oracles, which cannot act on the world, are the only things that decide. The planner is shown the catalog of oracles — their names, input shapes and grades — and never their implementations, never their results, and never a chance to revise one after seeing what it returned.

Reasoning is scoped to the run in focus and updates as the run proceeds. It is organised by phase, and each phase holds the steps that ran inside it: the stage, a one-line summary written by the engine, the model's stated rationale, the options it considered and rejected, which model family and role produced it, what it cost, and hashes of the inputs and outputs so the step can be found in the ledger.

pending

Planned, not started.

running

In progress now.

done

Finished and its output accepted.

refused

The step declined to produce something weak. A refusal is a result in its own right — see oracle synthesis.

failed

The step could not complete.

skipped

Not needed — usually because a cheaper path already answered the question.

Where the engine did not record something — a rationale, a token count, an escalation — the view says so rather than inventing a value.

A rationale is model output. It is shown as text, never as markup, and it is truncated with an affordance to open the full value. Nothing in the interface acts on it.

Treat it the way Certus does: as an account of why a plan was shaped this way, useful for judging whether the plan asked the right question. It is not evidence, and a confident rationale attached to an inconclusive obligation does not make the obligation any less inconclusive.

Every model call passes through a broker that redacts before anything is stored. Leased credentials, access keys, private keys and control-plane tokens are replaced, and the record keeps the rule that fired and the position — never the value. There is no per-call override for this, because one mistaken argument would be a key permanently stored in a content-addressed ledger.

Four roles call a model, and no output from any of them can become a PASS.

plan

Authors the proof plan, which is then statically validated.

challenge

Attacks the finished evidence. It may only add obligations or lower a grade — never upgrade one, never clear debt.

review

Summarises, and serves as the lowest-grade judge. It cannot mark a finding verifiable.

salvage

One bounded retry after a plan exhausts validation or a challenged obligation fails.

The planner and the challenger always run on different model families. Not different keys, accounts or temperatures — different families, because correlated errors are the failure mode this exists to prevent. When only one family is reachable, Certus does not quietly run both roles on it: the run is labelled as having had deterministic pre-checks only, and a claim whose policy requires a model challenge is blocked instead.

The challenger is deliberately kept ignorant of the planner's reasoning. It receives the claim, the plan, the oracle results and evidence summaries, and answers one question: under what plausible reading does this evidence fail to establish the claim? It does not see the planner's rationale, because if the planner never considered a question its rationale contains no trace of it — and a challenger reading that rationale would inherit the blind spot silently.

Findings carried forward from earlier runs are model-derived and therefore untrusted. Where they are shown to a model at all, they arrive as labelled data in a separate region of the message — never concatenated into instructions — carrying a normalized summary, an anchor, a severity and a confidence, and nothing else.

Raw statements as written, file contents, code excerpts, log lines, stack traces, diff hunks, evidence artifacts, URLs, hosts, email addresses, IP literals, human free text, and anything belonging to another repository never cross into a model's context under any role or setting.

Only the two static-review tasks may receive such a projection at all. Plan compilation, the challenger and the world researcher receive none — the challenger because feeding it the same prior would correlate its errors with the miner's, and the researcher because it is the one task with network access, which is the worst thing to pair with a durable attacker-writable channel.

A rationale that sounds like a verdict

It is not one, and nothing downstream treats it as one. Check the obligation's status and grade; those are the result.

The run shows deterministic pre-checks only

Only one model family was reachable, so no independent challenger could run. Add a second provider, or a gateway key that reaches more than one family.

A step marked refused

Synthesis declined to build a weak instrument. Read what it says would prove the claim — that list is the actionable part.

A plan that solved the wrong problem

Look at the rejected alternatives on the step. They usually show where the decomposition went wrong, and the claim's type is the most common cause.

Grade E appearing routinely

Model judgement is being used as an ordinary oracle. Set your policy to forbid model-only claims; it is the default for a reason.