Documentation
The console shows you what a run did. These pages say what each of those words means, what every value it can print stands for, and what to do when one of them surprises you.
Proof
- ClaimsA claim is one falsifiable statement about a change. Certus proves claims, not pull requests.
- ObligationsAn obligation is one provable requirement of a claim. Obligations are what oracles prove, and what a run can leave open as proof debt.
- VerdictsA run ends in one of five statuses. Three of them are not passes and not failures, and Certus never collapses them into either.
- GradesA grade says how much interpretation stands between the evidence and the claim. It is not a confidence, and it is never a percentage.
Execution
- SubstrateEvery run boots two sandboxes — one at BASE, one at HEAD. The Substrate view shows how each was provisioned and how it is functioning.
- SnapshotsBooting two environments per run would be slow if each started from nothing. Six cached tiers make most of a boot a restore.
- Trust domainsThree separated domains do the work of a run. What each is allowed to be wrong about is what keeps a model's opinion out of a PASS.
- EgressA sandbox can install what it needs, or it can run a proof. Never both at once. Egress happens in two phases, and the second one closes the registries.
Reasoning
- ReasoningThe Reasoning view is the model's working: what it decomposed, what it chose, what it rejected and why. Nothing in it is a result.
- PlanningBetween a claim and a proof sits a plan: a frontier to prove it at, and a declarative program that does the proving. Neither is written by hand, and neither is trusted.
- Oracle synthesisAn oracle is the instrument that takes the reading. Synthesis builds it — starting from the simplest thing that could work, and climbing only when it must.
Record
Setup
- RepositoriesConnecting a repository installs an app with a deliberately small set of permissions, binds it to your workspace, and starts the first index.
- EnvironmentOne contract per repository states what your application requires of its operator. It is the sole authority over which variable names exist in any sandbox Certus runs.
- IndexCertus reads your repository into a layered model of what it contains and how it connects. Everything downstream — the diff, the claims, the frontier — is derived from it.
- PolicyYour repository decides what “good enough to merge” means, in a file you review like code. Certus never picks the bar for you.