Bounded-set conjunction screening for satellite collision avoidance. A probability of collision answers "how much density falls inside the hard-body circle?". Certus asks a different question: given every state the declared covariance admits, can any admissible pair come within the combined hard-body radius during the screening window?
Usage guide · Architecture · Safety contract · Phase 3 handover · Phase 4 report · Phase 4 remediation · Corpus sweep · Gate power · Decision records
Important
Certus produces a conditional verdict about a declared set under a declared dynamics model. It is not a prediction that a collision will or will not occur, and every verdict is only as good as the covariance, the sigma multiplier k, and the Clohessy–Wiltshire validity envelope it rests on. Every condition is enumerated in docs/scope_note.md.
Note
The concept note's full ten-week build plan — phases 0 through 7 — is implemented: scope, ingestion, the Pc control arm, sound set propagation, the decision procedure, its refinement loop, its certificate and replay layer, and a real-corpus evaluation. docs/phase_4_report.md is that evaluation. The concept note's own "near/medium/longer term" extensions (manoeuvre synthesis, constellation-wide screening, covariance realism, extended-horizon dynamics) are future work, not part of this scope, and are not claimed here.
The conventional short-encounter probability of collision is not wrong, but it is fragile in a specific way. Hold the miss geometry fixed and scale the covariance: Pc rises, peaks, then falls toward zero. A very poorly tracked object and a very well tracked one can produce the same small number. Balch, Martin and Ferson call this false confidence, and it is a property of the metric rather than a bug in anyone's implementation.
Bounded-set reasoning separates the two cases that Pc blurs together — clearance of the entire declared set, versus unresolved possibility inside it — at the cost of deliberate conservatism and possible indeterminacy.
That makes the engineering problem unusual:
- The answer must be sound, not accurate. A bound that is 10% loose is useful. A bound that is 0.001% optimistic is worthless. Every operation is an over-approximation with a proof.
- Floating point is part of the proof obligation. Every binary64 matrix product, generator sum and midpoint conversion carries a derived outward error bound. The one remaining axiom is stated narrowly and in one place: platform
sin/cosland within one adjacent representable value. - Time is enclosed, not sampled. The bound holds over the whole continuous window because each closed interval's state-transition matrix is bracketed elementwise — not because a grid was checked finely enough.
- The gates are mutation-tested. Thirteen mechanical defects are injected into the claimed path only; the truth path is built first and never mutated. The suite is scored on how many it catches, including the ones it does not.
- Solvers are not trusted. Clarabel proposes a direction; a directed-rounding certificate verifies it. A solver stall costs tightness, never soundness.
- Unfavourable numbers are published. The corpus sweep reports that the bound decides 37.74% of real conjunctions, and that the cheap filter decides 7.55%. Those numbers contradict the design's original premise and are reported anyway.
flowchart LR
A["CCSDS CDM<br/>strict KVN/XML"] --> B["Canonical record<br/>SI at the boundary"]
B --> C["RTN covariance<br/>rotated per object"]
C --> D["k-sigma ellipsoids<br/>X_p, X_s"]
D --> E["Relative state set<br/>mu + E(F_s) - E(F_p)"]
E --> F["Interval CW STM<br/>over each closed interval"]
F --> G["Ellipsoid image<br/>+ one coordinate box"]
G --> H["SOCP support dual<br/>Clarabel + certificate"]
H --> I{"lower > R ?"}
I -->|yes| J["interval CLEARED"]
I -->|no| L{"sampled point ≤ R ?"}
L -->|yes| M["CONFLICT_WITNESSED<br/>+ replayable witness"]
L -->|no| N["bisect the interval"]
N --> F
J --> O{"whole window covered ?"}
O -->|yes| P["PROVEN_CLEAR<br/>+ replayable certificate"]
O -->|no, budget spent| Q["INDETERMINATE"]
The certified path never builds a zonotope. A linear map of an ellipsoid is an ellipsoid, so A·{Fu : ‖u‖₂ ≤ 1} = {(AF)u : ‖u‖₂ ≤ 1} is exact; the only enlargement is a single coordinate box carrying the interval-STM remainder and the rounding of the midpoint products. The state existential this produces is exactly convex, so it is decided by the same certified SOCP oracle throughout, not handed to a general SMT solver — ADR 014 is the design record for that choice, backed by a measured Z3 scaling wall on the same problem.
Python 3.11 or newer. Runtime and development dependencies are exactly pinned.
python3 -m venv .venv
. .venv/bin/activate
python -m pip install --upgrade pip
python -m pip install -e '.[dev]'Run the fast verification suite — lint, strict types, and 159 unit tests:
make checkDecide one real CDM, end to end, and write a replayable certificate:
certus-decide decide path/to/one.cdm --output cert.json
certus-decide verify path/to/one.cdm cert.json # standalone, solver-free replayTwo committed, physically plausible example CDMs to try this on immediately —
docs/examples/easy_clear.cdm and docs/examples/contested_conflict.cdm — and
a full walkthrough with every command's real captured output, including what
INDETERMINATE and a rejected tampered certificate actually look like, are in
docs/USAGE.md.
Ingestion fails loudly on malformed schemas and converts to SI at the boundary.
certus-normalize cdm path/to/one.cdm path/to/two.cdm --output data/cdms.parquet--hbr-m is mandatory for the ESA Kelvins table, which contains no unambiguous combined hard-body radius. Certus never invents one; Kelvins records preserve their missing absolute TCA, inertial states and RTN bases as named gaps, so they cannot reach the frame-correct gates.
Three provenance-locked NASA CARA conjunctions, k = 3, a ±300 s window and 6,000 closed intervals. tightness is the certified bound over the exact ellipsoid-set grid minimum — 1.0 would mean no conservatism at all.
| Case | Zonotope bound (ADR 007) | Ellipsoid bound (ADR 012) | Recovered | Tightness |
|---|---|---|---|---|
…055818 |
1,374.667184 m | 1,379.482337 m | +0.350278% | 0.985137 → 0.988588 |
…232706 |
297.879557 m | 311.390804 m | +4.535809% | 0.956464 → 0.999847 |
…145954 |
181.998752 m | 202.775129 m | +11.415670% | 0.897515 → 0.999973 |
Removing the coefficient-box relaxation from the bound path recovers two to eleven percent and takes two of three cases to within 0.02% of the exact answer. Case A is interval-time limited, not shape limited: its 64.75 m box is almost entirely the real-arithmetic remainder, so this change could not help it.
The bound was run over every conjunction the ingest layer can complete — all 53 CARA records, none excluded.
| Decision path | PROVEN CLEAR |
Fraction |
|---|---|---|
| Certified ellipsoid bound, one conic solve per interval | 20 / 53 | 37.74% |
| Cheap box filter, no solver at all | 4 / 53 | 7.55% |
32 of 53 records return an exactly zero bound and only 4 sit in the contested band bound/R ∈ [0.1, 10]. The distribution is strongly bimodal — a conjunction is usually either hopeless for a set bound or clear by two to three orders of magnitude.
This contradicts the assumption the project started from, which was that the cheap bound decides most cases. It decides 7.55%. The regime a solver exists for is the majority of this corpus, not an edge case. Full analysis and the exclusion ledger: docs/corpus_sweep.md.
Thirteen mechanical defects against seven cases, on both declared propagation paths.
| Gate 3.1 stage | Required mutation-case cells | Cost |
|---|---|---|
| Box containment (previous baseline) | 47 / 77 | — |
| Sample escape (now a secondary diagnostic) | 56 / 77 | 1,478.6 s |
| Zonotope support envelope | 61 / 77 | — |
| Ellipsoid support envelope | 77 / 77 | 9.4 s |
Two defects — a claimed set scaled by 1.25, and one with a spurious extra factor column — are invisible to every sampling-based test by construction: a set that is too large contains every sample. 11.4 billion escape comparisons found nothing. The two-sided envelope catches both on all seven cases at the first epoch.
The deciding stage costs 9.4 s where its predecessor spent 15.6 billion comparisons and 375,577 LP solves. Its power comes from an algebraic identity rather than sample density, so it does not depend on seed, sample count, set size, or window length. Full matrix: docs/gate_power.md.
certus.decide.decide_conjunction answers the safety property directly rather than only bounding it — the same certified oracle above, wrapped in interval bisection over time, short-circuiting the instant a genuine violation is found. Run on the full 53-record CARA corpus, k = 3, budget max_solve_count=8,000:
| Verdict | Count |
|---|---|
PROVEN_CLEAR |
22 |
CONFLICT_WITNESSED |
31 |
INDETERMINATE |
0 |
Every one of the 53 certificates replayed successfully against verify_certificate — a solver-free checker that rebuilds interval images and evaluates stored feasible support directions for clearance, or reconstructs a concrete original state for conflict. Total generation cost: 2,295 solves and 15.22 s of wall clock for the whole corpus, versus a single fixed-time instant of the same problem timing out unresolved after 6 s under Z3's nlsat at a quarter the real dimension (docs/decisions/014).
Refinement recovers real cases the fixed-partition bound alone could not close, with zero regressions — every record the plain bound already proved clear is still proved clear:
| Record | Fixed-partition bound/R |
Refinement result |
|---|---|---|
...154111 |
0.5485 (not proven clear) | PROVEN_CLEAR, 66 solves |
...154409 |
0.0000 (touches zero on the grid) | PROVEN_CLEAR, 146 solves |
Against the conventional Pc control, 15 of 53 records (28%) are CONFLICT_WITNESSED while Foster Pc sits below a conventional 1e-4 action threshold — the dilution-candidate class the concept note names as the core value proposition. This is not 15 missed collisions: most of these witnesses sit at the 1e-11 m scale, meaning the declared k=3 uncertainty region contains the origin outright, which is a measured fact about how conservative bounded-set reasoning is at this k, not a claim about what happened to these satellites. The opposite direction is reported too — 4 records where Pc crosses the threshold but Certus proves the whole window clear, each needing genuine refinement (7–12 levels deep), not a trivial pass. Full method, every number, and the caveats that go with them: docs/phase_4_report.md.
make acceptanceExpect 9 passed and 1 strict expected failure in roughly 80 minutes. The expected failure is the literal Gate 2.1 Foster–Chan assertion, which is superseded rather than passing — see ADR 003. Individual gates and figure regeneration:
PYTHONPATH=src pytest -q tests/acceptance/test_phase_3_gates.py -k gate_3_2 -ssrc/certus/
types.py canonical records, SI units, immutable arrays
roundoff.py directed binary64 arithmetic, Higham + directed radii
ingest/ strict CCSDS CDM and ESA Kelvins loaders, Parquet output
frames/ RTN bases, per-object rotation, encounter plane
baseline/ Foster quadrature, Chan series, Serra series, dilution
sets/
ellipsoid.py k-sigma ellipsoids, explicit non-PD handling
zonotope.py outward-rounded maps, kept as the fast filter
distance.py SOCP support duals with directed-rounding certificates
support.py two-sided support-envelope comparison
membership.py finite support checks, LP membership
dynamics/
cw.py Clohessy–Wiltshire state-transition matrix
interval.py analytic interval STM enclosures, ellipsoid images
bounds.py continuous-window bounds + original-state witness replay
relative.py record to relative-state uncertainty
decide/
certificate.py Verdict, Witness, DecisionCertificate (de)serialisation
engine.py decide_conjunction: convex-native encoding + refinement
replay.py verify_certificate: standalone, solver-independent audit
z3_cross_check.py optional independent QF_NRA cross-check (pip install certus[z3])
cli.py certus-decide decide / certus-decide verify
Every design change carries an architecture decision record. The ones that matter most:
| ADR | Decision |
|---|---|
| 005 | Zonotope relaxation, re-scoped to a filter after its cost was measured |
| 007 | Continuous time by interval STM enclosure, not by grid refinement |
| 008 | Outward-rounded arithmetic; the one remaining sin/cos axiom |
| 009 | Conic oracles replace Monte Carlo as the tightness reference |
| 012 | The certified path is ellipsoid-native, so k stays the operator's k |
| 013 | Two-sided support envelope; sample escape demoted to a diagnostic |
| 014 | The decision engine is convex-native; Z3 is a bounded cross-check, not the engine |
k = 3is a test choice, not an operational policy, and not a claim of 99.7% coverage in six dimensions. It is also why 15/53 corpus records areCONFLICT_WITNESSEDwith the origin essentially inside the declared set — a differentkwould give a different, equally honest, answer to a differently-sized question.- Covariance realism is unverified. Certus checks matrix validity, not whether the covariance describes the true state error. A sound verdict about the wrong set is still the wrong answer.
- CW validity is narrow: near-circular primary, small relative separation, no manoeuvres, short window. 52 of 53 corpus records satisfy it; one does not and is retained with the caveat recorded rather than dropped.
- One arithmetic axiom remains. Platform
sin/cosare assumed to land within one adjacent representable value of the exact real. Neither correct rounding nor a strongerlibmguarantee is claimed. - One mutation is caught by nothing. Removing outward rounding from the claimed interval hulls (M9) changes values at the ULP level while geometric margins are metres to kilometres.
- Gate 3.1 probes 262 frozen directions, not all of them, and checks 61 epochs rather than continuous time. The bound encloses continuous time; the containment gate does not.
- The corpus is 53 records. ESA Kelvins contributes 0 usable records out of 24,484 because it omits absolute TCA, both inertial states and both RTN bases.
INDETERMINATEis implemented and tested, not merely theoretical, but did not occur on this corpus at this budget. A harder or adversarially-constructed case should be expected to reach it;docs/phase_4_report.mddoes not claim otherwise.- The Z3 cross-check is genuinely limited, not just cautious. Measured on this host, two generators per object (4 real variables) already times out against
nlsatwith realistic CW-propagated coefficients; the real fixture's six-per-object encoding does not resolve at any budget tested. It validates the SOCP encoding at the scale it can reach and is honest about the rest — seedocs/decisions/014. - No manoeuvre verification, constellation-wide screening, or covariance-realism preprocessing. These are the concept note's own "near/medium/longer term" extensions beyond the ten-week core plan, and are out of scope here by that document's own scoping, not by omission.
Certus is decision-support for conjunction assessment, a domain where a wrong answer has physical consequences. Every verdict — PROVEN_CLEAR, CONFLICT_WITNESSED, or INDETERMINATE — is conditional on inputs no software can validate, covariance realism above all. None is a substitute for an operator's judgement, and the conventional Pc control arm is retained precisely so the two can be compared rather than one silently replacing the other.
Report a suspected soundness defect — any case where a bound may be optimistic — through SECURITY.md. Development conventions, including the non-negotiable rules about never loosening a threshold to make a test pass, are in CONTRIBUTING.md.
Proprietary. All rights reserved. See LICENSE.
Gate fixtures are derived from public CDMs in NASA's nasa/CARA_Analysis_Tools at commit 86ba28ad2ae6acacff29df5933809e731f500935, each carrying its source SHA-256. The ESA Collision Avoidance Challenge archive (10.5281/zenodo.4463683) is referenced but not redistributed.