Planning

A run moves through eight stages. Planning is one of them, and most of what the Reasoning view shows happens inside it.

trigger

A pull request, a CLI invocation, or an MCP tool call starts the run.

index

BASE and HEAD are indexed into a software model. See index.

analyze

The two models are diffed into a change graph, the change is classified, and claims are derived and reconciled.

frontier

A verification frontier is selected per claim — how far this change can honestly be exercised.

plan

Each claim is compiled into a validated proof plan.

execute

The plans run on both twins, producing evidence.

judge

Oracles read the evidence, and the challenger attacks the result.

verdict

Everything folds into one signed verdict.

A stage can end as succeeded, failed, inconclusive or blocked, and those four are never collapsed into each other.

Classification decides the whole strategy, so it happens first and deterministically. There are nine classes, and rules are evaluated in a fixed order with the first match winning.

A · full feature

New code reachable from a boundary, with every declared claim realizable. Proved end to end, with a mandatory negative control on BASE.

B · partial

Backend-only, migration-only or scaffolding. Proved at the highest realizable internal frontier; the rest becomes proof debt.

C · completes a feature

A small change makes previously dangling code reachable, and open debt exists for that feature. Everything deferred comes due now, whatever the line count. This is the case a size heuristic always misses.

D · bug fix

A reproduction is synthesized and a differential oracle is mandatory: it must fail on BASE and pass on HEAD.

E · refactor

No interface delta and no declared behavior change. Proved as BASE/HEAD equivalence over generated inputs, with coverage evidence that those inputs reached the changed code.

F · dependency, config or infrastructure

Both sides boot, existing tests run, contract snapshots are diffed, and added dependencies are checked for advisories.

G · tests or docs only

Run on both sides, checking that new tests exercise what they name and fail against mutated code.

H · data migration

Twin databases seeded identically, the migration applied, then invariants, reconciliation, and a down-migration round trip.

I · mixed

Several unrelated components in one change. Split, classified separately, and proved separately under one verdict.

The class is shown to you and you can correct it. A correction re-plans the run rather than editing the verdict, because a wrong class is the commonest cause of a wasted run — and the one error you will spot in two seconds while Certus spends ten minutes failing to discover it.

A model is consulted for exactly one thing here: breaking a tie between bug fix and refactor. That is recorded as a model judgement, never as an assertion, and the classification's confidence drops to say so. If no model is available, deterministic precedence decides.

A frontier is not a single place in the code. It is a bounded slice of executable behavior: entry points the harness can drive, terminal observations it can read back, everything reachable between them, and — importantly — a recorded reason for every path that was cut out.

Cutting a branch without recording why would make “we excluded nothing” unfalsifiable. So every cut edge produces one exclusion record naming the concrete artifact and what would fix it.

Frontiers sit at one of eight levels, and the level is orthogonal to what kind of boundary is being driven. A level never caps a grade; it describes how much of the real system was involved.

function

One unit invoked directly. No framework, no process, no transport.

component

The unit exercised through the application's own wiring — routing, middleware, serialization.

contract

Only the published interface and conformance to it. Nothing behind the interface is asserted.

service

One deployable unit booted as a real process against its own real state store.

integration

Two or more real participants composed across a process boundary. A service and its own database do not count as two.

application

Every participant the product needs, driven at its outermost machine-facing entry.

user

A human-equivalent driver performing the human's own sequence — a real browser, a terminal, an assistant client.

external reality

At least one observation reads state back from a system outside the deployment that this run changed.

Certus reaches for the largest slice it can realize, not the deepest one it can touch. A frontier is scored on how much of the changed behavior it covers, how observable it is, how realistic it is and how confident the paths are — against what it costs to set up, what it costs to run, how flaky it is, and how many dependencies are unresolved. The scoring has no tunable weights.

A plan is declarative data, not a script: a claim, a frontier, an environment, fixtures, a graph of steps, the observations to capture, the oracles to apply, a negative control, the evidence required, and a budget. References between steps are expressions that select and project; they cannot branch, loop, call out, or compute a value nobody observed.

That is what makes a plan schedulable on both twins at once, cacheable, hashable, diffable, checkable before it runs, and replayable afterwards. It is also what makes the artifact — rather than the model that wrote it — the thing a verdict rests on.

Arbitrary code is admitted in exactly two places. A sandbox command may run with declared effects and produce typed output — and it may assert nothing; an exit code of zero is not an oracle. An oracle program may compute a result over declared evidence, with no network, a pinned interpreter and a tiny library allowlist — and it does not learn which side it ran on, what the claim says, what the plan was, or what any other oracle returned. There is no third place.

Every plan is checked before anything executes. The checks exist because each catches a specific fake proof that reads convincingly.

• A step calling a capability that does not exist, or with inputs that do not fit it — which would be silently dropped at run time.
• A claim with no oracles at all: a plan that exercises the feature beautifully and asserts nothing. This is the commonest planner failure and the most convincing one to read.
• A claim resting only on model judgement, unless your policy allows it and the plan states a reason.
• A new-capability or bug-fix claim with no negative control on BASE — a proof of behavior that already worked.
• A cycle in the step graph, which would hang mid-budget.
• A reference to a step, fixture or output that does not exist, which would resolve to nothing and compare nothing to nothing — silently, and it would pass.
• A step whose effects exceed what the frontier permits: a user-interface claim reaching into the database to arrange the state it then observes.
• An estimated cost over the claim's budget, which would be killed mid-flight.
• An oracle requiring evidence no step produces, which would fail at run time and read like a product bug.

A rejection is structured — the rule, the step or oracle, and a suggested fix — and the planner gets three attempts to satisfy them. After that the claim is INCONCLUSIVE: unplannable and becomes proof debt.

There is no fallback to a weaker plan. A system that quietly substitutes “the test suite was green” for “we could not construct a proof of this claim” launders a failure to plan into an appearance of evidence.

The selected frontier is a hard precondition on the plan, not a suggestion. A plan may not drive an entry point outside it, observe something that is not a terminal observation, name an excluded branch, cover less than it declared, or fail to consume evidence from any terminal observation at all.

A violation carries one of two redresses, and the difference is the most actionable thing in the whole subsystem. Replan means the planner made an ordinary mistake and the bounded retry loop will handle it. Refer to frontier means the frontier is wrong, not the plan — replanning will not help, and something about the environment, the observation method or the boundary fidelity has to change.

Policy can narrow what frontiers are admissible. It cannot widen them. Widening is not a permission Certus withholds; it is a sentence the system cannot express. A fidelity floor can only be raised, because a knob that lowers a floor is a knob that buys a grade.

INCONCLUSIVE: unplannable

Three plans were rejected. Read the rejections: each names a rule and a suggested fix. The claim is carried as debt, not dropped.

A violation whose redress is “refer to frontier”

Fix the environment, not the plan. The frontier asked for something the slice, the recipe or a dependency policy does not provide.

The claim was proved somewhere smaller than you expected

Read the excluded branches. Three of the reasons are directly actionable: a frontier you forbade in policy, an external dependency with no policy assigned, and a component that would not boot on both twins.

No frontier was admissible at all

Usually self-inflicted: check the never list in .certus/policy.yaml. Policy can only narrow, so an over-broad entry removes every candidate.

The wrong class

Correct it. The run re-plans from the new class rather than patching the verdict.

The two twins started different components

Never accept the verdict. A differential over asymmetric environments measured the environment, not the change — and Certus blocks rather than reporting it.