Autonomous, contract-driven Space Traffic Management for the Kessler era. A complete end-to-end satellite conjunction-screening and collision-avoidance system written in Ada/SPARK, with a web UI that renders real NASA satellite imagery and live orbital state.
On "formal verification": the safety-critical numerical core is written in the SPARK subset with
Pre/Post/range contracts so it can be discharged bygnatprove(see the Verification section). The contracts are in place; running the prover to a given assurance level is a build step the operator performs — this repository ships the analysable code, not a stamped proof certificate.
Low Earth Orbit is becoming unmanageable. As of 2024 the U.S. Space Force tracks roughly 30,000 resident space objects (RSOs); estimates of objects too small to track sit above 130 million. One major break-up event in a populous shell can trigger a runaway debris cascade (the Kessler Syndrome) which would render a large altitude band unusable for generations.
Most operational conjunction-analysis systems — CARA at NASA/GSFC, LeoLabs' commercial offering, and several proprietary ESA tools — are closed source or run only inside agencies. Orbital Shield is an open, auditable alternative built on the same published algorithms:
- SGP4 / SDP4 orbital propagation in SPARK Ada (WGS-72, Hoots/Roehrich + Vallado-2006 corrections), covering both near-Earth and deep-space regimes.
- All-pairs conjunction screening with apogee/perigee pre-filtering and golden-section TCA refinement.
- Foster's 2-D Simpson method for collision probability
Pcwith age-dependent covariance synthesis from TLE epoch. - Clohessy-Wiltshire collision-avoidance manoeuvre planner that emits sign-correct along-track Δv recommendations with verifiable Pc reduction.
- A hand-rolled HTTP/1.1 server using
GNAT.Sockets, exposing a JSON REST API. - A Three.js front end rendering the real Earth from NASA Blue Marble (MODIS) and Black Marble (Suomi-NPP VIIRS) composites with live satellite positions, classified by type, plus conjunction links coloured by risk level.
The Ada layer is partitioned with SPARK_Mode => On for the
safety-critical numerical core (Vector_Math, Time_Utils,
SGP4_Propagator specs) and SPARK_Mode => Off for the I/O and
networking edges — the standard pattern for high-integrity systems.
orbital_shield/
├── orbital_shield.gpr GNAT project
├── src/
│ ├── orbital_shield.adb Main orchestrator + screener task
│ ├── core/
│ │ ├── orbital_types.ads Real, vectors, TLE, events, plans
│ │ ├── vector_math.{ads,adb} 3-D linear algebra, safe trig
│ │ └── time_utils.{ads,adb} Julian date, GMST, ISO time
│ ├── propagation/
│ │ ├── sgp4_propagator.{ads,adb} SGP4 init + propagate
│ │ ├── tle_parser.{ads,adb} Two-line-element decoder
│ │ └── catalog.{ads,adb} Object catalog management
│ ├── analysis/
│ │ ├── conjunction_analysis.{ads,adb} Screening: grid + sweep-prune
│ │ ├── collision_probability.{ads,adb} Foster 2-D Pc
│ │ ├── history.{ads,adb} Pc trend tracking + persistence
│ │ └── maneuver_planner.{ads,adb} CW Δv optimiser
│ └── io/
│ ├── json_output.{ads,adb} Encoder
│ ├── engine_state.{ads,adb} Protected shared state
│ ├── alerts.{ads,adb} Webhook push on critical Pc
│ └── http_server.{ads,adb} HTTP/1.1 listener
├── web/
│ ├── index.html UI layout
│ ├── style.css Dark space theme
│ ├── globe.js Three.js scene (real NASA imagery)
│ ├── app.js Backend client + live Celestrak engine
│ └── cdm.js CCSDS 508.0-B-1 CDM (KVN) builder
├── tools/
│ └── fetch_catalog.py Celestrak ingestion (checksum + de-dup)
├── tests/
│ ├── tests.gpr Test build project
│ ├── sgp4_verify.adb SGP4 reference-vector check (SGP4-VER)
│ ├── sdp4_verify.adb SDP4 deep-space parity vs satellite.js
│ ├── screen_verify.adb Spatial pre-filter exactness + scaling
│ ├── history_verify.adb Pc-trend detection + persistence
│ ├── pc_verify.adb Foster Pc integral vs closed-form + quadrature
│ ├── mc_verify.adb Monte-Carlo Pc vs Foster + Rayleigh + RK4 CW
│ ├── time_verify.adb JD/ISO time conversions, day-sweep + round-trip
│ ├── init_verify.adb Initialize contract + catalog resilience
│ ├── maneuver_verify.adb CW along-track sizing singularity guard
│ ├── tle_verify.adb TLE field decoding (incl. Alpha-5 catalog numbers)
│ ├── json_verify.adb JSON number-formatting magnitude guard
│ └── cdm_verify.mjs CCSDS 508.0-B-1 CDM conformance (Node)
├── data/
│ └── sample_catalog.tle Celestrak-format real TLEs (checksum-valid)
└── README.md
Install GNAT and Alire (recommended) on Windows/Linux/macOS:
# Windows (winget)
winget install AdaCore.GNAT
# macOS (Homebrew)
brew install gnat
# Or via Alire (cross-platform)
curl -L https://alire.ada.dev/install.sh | shThen from the project root:
gprbuild -P orbital_shield.gprThis produces bin/orbital_shield. Build modes:
gprbuild -P orbital_shield.gpr -XMODE=release # -O2 optimised
gprbuild -P orbital_shield.gpr -XMODE=debug # -O0 -gnata checks
gprbuild -P orbital_shield.gpr -XMODE=prove # check-syntax onlyTo run the SPARK proof tooling over the contract-annotated core
(requires gnatprove; see the Verification section for what is and
isn't discharged):
gnatprove -P orbital_shield.gpr --level=2 --prover=cvc5,z3,altergoOrbital Shield runs the same algorithms in two places:
- Backend mode — the Ada/SPARK engine is the authoritative source. It runs the SGP4 propagator, conjunction screening, Foster Pc and the CW maneuver planner, and serves both the UI and a JSON API. The HTTP listener binds to 127.0.0.1 only (operator console, not a public service).
- Live mode — if the browser UI is opened without the backend, it
ingests the real current catalog directly from Celestrak's GP API
and propagates it client-side with
satellite.js(a faithful SGP4/SDP4 implementation), running the identical screening + Pc + CAM logic. Switch catalog groups (debris clouds, Starlink, stations, …) live from the dropdown.
Either way the data is real — no synthetic catalog in normal use.
# Real catalog shipped with the repo (checksum-valid TLEs)
./bin/orbital_shield data/sample_catalog.tle
# Custom port
./bin/orbital_shield data/sample_catalog.tle 8080
# No file -> synthetic LEO shells (offline demo / CI only)
./bin/orbital_shieldOn startup the server blocks until the first screening cycle completes,
then opens the listener. Visit http://localhost:8080.
Use the bundled ingestion helper, which validates checksums and de-duplicates by NORAD id:
python tools/fetch_catalog.py --list # known groups
python tools/fetch_catalog.py stations fengyun-1c-debris # -> data/live.tle
./bin/orbital_shield data/live.tle(curl works too, but fetch_catalog.py enforces the same checksum
rules the Ada parser does, so the backend won't silently drop rows.)
The catalog dropdown groups objects by propagator:
- Low Earth orbit (SGP4) — period < 225 min: Fengyun-1C debris, Cosmos-2251 / Iridium-33 debris, Starlink, the space stations, the last-30-day launches, the active LEO catalog.
- Deep space (SDP4) — period ≥ 225 min: the entire geostationary belt (~570 active objects), GPS / GLONASS / Galileo / BeiDou MEO constellations.
satellite.js automatically routes objects to SGP4 or SDP4 based on
the recovered mean motion. In live mode the frontend also adjusts its
own screening parameters to match the regime — deep-space defaults are
a 48 h horizon, a 120 s coarse step (relative motion is ~10× slower
than LEO) and a 200 km screening volume (deep-space covariance is ~10×
larger and operators screen at wider thresholds); the Ada backend runs
one fixed Screen_Config (24 h / 60 s / 25 km) regardless of regime.
Asset classification covers both regimes too — pick GOES-16 or TDRS-3
as your protected asset and screen it against the GEO belt to surface
real co-location encounters.
Status of the Ada backend SDP4: implemented.
SGP4_Propagatornow runs the full unified SGP4/SDP4 model — deep-space objects (period ≥ 225 min) are propagated with luni-solar secular and periodic perturbations (dscom/dpper) and geopotential resonance integration for both synchronous (one-day) and Molniya/half-day orbits (dsinit/dspace). The port mirrors the canonicalsatellite.jsroutines function-for-function, so the Ada backend and the browser live mode produce identical deep-space states. This is verified bytests/sdp4_verify(see Verification), which matchessatellite.jsto below display precision across all three resonance regimes.
The default screening mode is within-catalog (every object against every other in the chosen group). Switch the Screening mode dropdown to Asset → catalog to run the workflow real conjunction-assessment teams use:
- Pick a protected asset from the dropdown — ISS, Hubble, Aqua, Terra, Landsat 8, the Sentinels, Suomi NPP, Tiangong, or any custom NORAD id.
- The frontend fetches that object's TLE directly from Celestrak's
single-object
CATNRendpoint and propagates it on a fine 24 h grid. - Each object in the chosen threat catalog is streamed against the asset's grid, with an apogee/perigee pre-filter so altitude-disjoint pairs cost nothing. This is O(N) instead of O(N²) — it scales to the full active catalog.
- Surviving pairs are TCA-refined and Pc'd, and (because the asset is maneuverable) the planner emits CW Δv proposals only for the asset's side of every encounter.
Example end-to-end: select Aqua (27424) vs the Fengyun-1C debris cloud and the engine surfaces real close approaches around the A-Train altitude band, including warning-level events with sub-3 km miss distances — and recommends a sub-1 m/s along-track burn ~2 h before TCA that drives the Pc into the floor.
The protected asset is drawn in gold in the 3-D scene at 8 px (vs ~3 px for ordinary catalog objects) so it's easy to spot in a debris cloud.
The scene has a time-scrub timeline at the bottom: drag the slider from −1 h to +24 h to advance the satellite catalog in time, hit ▶ to auto-play (1 min/s · 10 min/s · 1 h/s · 4 h/s), and click → TCA on any conjunction event to jump the timeline straight to that encounter's closest approach. Combined with the B-plane view this gives both the spatial and the temporal picture of an encounter.
Propagation during scrubbing happens client-side through the same satellite.js SGP4 that was verified against the official Vallado reference vectors.
Click any conjunction to open the encounter B-plane — the 2-D plane perpendicular to the relative velocity at TCA, the view conjunction analysts actually work in. It draws the combined 1/2/3-σ covariance ellipse at the projected miss point and the hard-body circle at the origin. Because the Foster Pc is the integral of that covariance over the hard-body circle, the visual overlap of the two is the collision probability — you can see at a glance why a 2 km miss with a 6 km along-track uncertainty is a "warning" while a 20 km miss is not.
A single collision probability is a snapshot; what an operator actually
watches is the trend. Each screening cycle the engine folds every
event's Pc into a per-pair rolling history and derives a direction —
climbing, falling or steady — plus the length of the current
run, so the UI can say "this Pc has been climbing for 3 cycles".
Every conjunction row shows a trend chip and a log-scale sparkline of its
recent Pc series.
The trend table is persisted to disk (data/history.dat) every cycle
and reloaded on boot, so the streak survives a restart — relaunch the
engine mid-event and a climbing Pc keeps counting up rather than resetting
to "new". Live mode mirrors this client-side, persisting per-group trend
state in localStorage. The trend fields (pc_trend, trend_cycles,
pc_prev, pc_series) are included in the /api/conjunctions JSON, and
the logic is verified by tests/history_verify (streak detection,
reversal, and a save/load round-trip).
Foster's 2-D method assumes a hyperkinetic, short, well-defined encounter
(see Operational alignment). For the events that violate that — flagged
low_rel_velocity or aged_covariance — the engine runs the
higher-fidelity cross-check NASA CARA uses for them: a Monte-Carlo Pc
that does not assume rectilinear relative motion. It samples the
combined 3-D position covariance and propagates each draw with curved
Clohessy-Wiltshire relative dynamics over a window around TCA, scoring
a hit when the minimum separation drops below the combined hard-body
radius. Only position uncertainty is sampled — no velocity covariance is
fabricated, matching the inputs Foster uses.
The result is surfaced as pc_mc in the /api/conjunctions JSON (and an
"MC" chip in the UI) for flagged events; nominal events report null (the
2-D Pc is trusted and the cost is skipped). Work is bounded — only the
most-dangerous flagged events are cross-checked per cycle (the rest keep
the 2-D Pc, logged when the cap bites) so a co-orbiting debris cloud cannot
stall screening. Live mode mirrors the same estimator client-side.
tests/mc_verify pins it down: in the hyperkinetic regime where Foster is
valid the estimator reduces to Pc_Circle and the closed-form Rayleigh
limit (within the binomial sampling band), and the curved Clohessy-Wiltshire
state transition it relies on is checked term-for-term against an
independent RK4 integration of the Hill equations.
The conjunctions panel has an Export CCSDS CDM button that writes a CCSDS 508.0-B-1 Conjunction Data Message (KVN) for every screened event — the mandatory header, relative metadata/data (TCA, miss distance, RTN-frame relative state, Foster collision probability), and for each object the metadata, TEME state vector and the full lower-triangular 6×6 RTN covariance (all 21 terms). This is the interchange format the 18th Space Defense Squadron and commercial providers distribute, so the output drops straight into standard conjunction-assessment tooling.
CDMs are advisory: each object's covariance is the position-only,
age-based covariance the screener uses (so the velocity block and the
off-diagonal position terms are zero), COVARIANCE_METHOD is reported
as DEFAULT, not CALCULATED, and INTERNATIONAL_DESIGNATOR is always
UNKNOWN (the TLE field it comes from isn't parsed on either side yet).
The builder lives in web/cdm.js and is checked against the Blue Book
mandatory field set, keyword ordering, enumerations and time format by
tests/cdm_verify.mjs (node tests/cdm_verify.mjs).
The backend can push a notification the moment a conjunction crosses a critical collision-probability threshold — no polling required. Arm it from the environment:
ORBITAL_SHIELD_WEBHOOK=http://127.0.0.1:9000/alert \
ORBITAL_SHIELD_PC_ALERT=1e-4 \
./bin/orbital_shield data/live.tleOn each screening cycle every event with Pc ≥ ORBITAL_SHIELD_PC_ALERT
(default 1e-4, the "critical" level) is evaluated. When a pair first
crosses the threshold the engine POSTs a JSON body to the webhook:
{"type":"conjunction_alert","state":"opened","primary":90001,"secondary":90002,
"pc":5.87e-08,"pc_threshold":1.0e-08,"miss_km":9.6005,"rel_speed_km_s":0.0105,
"tca":"2026-06-18T01:47:39Z","risk":"watch","pc_trend":"new","trend_cycles":0,
"generated_at":"2026-06-17T12:55:59Z"}It is edge-triggered with hysteresis: an alert fires once when it
opens and once ("state":"cleared") when the Pc falls back below
0.7 × threshold, never every cycle. The POST runs on a dedicated
dispatcher task fed by a bounded mailbox, so a slow or unreachable sink
can never stall screening — a failed POST is logged and dropped.
Only plain
http://is supported (GNAT.Socketshas no TLS), matching the loopback/intranet alert-sink model the rest of the engine assumes. For an internet endpoint (Slack, PagerDuty, …) point the webhook at a local relay that adds TLS.
| Path | Returns |
|---|---|
GET / |
Single-page web UI |
GET /api/status |
Catalog size, conjunction count, maneuver count, generated_at |
GET /api/catalog |
Propagated ECI states of every object in the catalog |
GET /api/conjunctions |
All predicted close approaches over the next 24 h |
GET /api/maneuvers |
Δv recommendations for events with Pc ≥ cutoff |
GET /<asset> |
Static asset from web/ |
The protected-object access pattern in Engine_State guarantees that
each API call sees a coherent snapshot — the catalog and conjunction
arrays cannot be mid-update when the responder reads them.
| Source | Used for |
|---|---|
| NASA Earth Observatory — Blue Marble Next Generation | Day-side Earth texture |
| NASA Goddard / Suomi-NPP VIIRS — Black Marble | Night-side city lights texture |
| NOAA / NGDC ETOPO1 | Topography bump map |
| Celestrak (Kelso et al.) | TLE catalogs |
| WGS-72 | Gravity model used by SGP4 |
NASA imagery is mirrored via the three-globe package CDN to keep
deployment self-contained. For an air-gapped or compliance-controlled
environment, download the JPEGs once and serve them from the local
web/ directory.
| Subject | Reference |
|---|---|
| SGP4 algorithm | Hoots & Roehrich, Spacetrack Report #3 (1980) |
| SGP4 corrections | Vallado, Crawford, Hujsak, Kelso, Revisiting Spacetrack Report #3 (AIAA 2006) |
| Collision probability | Foster, A Parametric Analysis of Orbital Debris Collision Probability (1992) |
| 2-D Foster integration | Akella & Alfriend, Probability of Collision Between Space Objects (2000) |
| CW relative dynamics | Clohessy & Wiltshire, Terminal Guidance System for Satellite Rendezvous (1960) |
| TLE covariance (at epoch) | Flohrer, Krag & Klinkrad, Assessment and Categorization of TLE Orbit Errors for the US SSN Catalogue (AMOS 2008) |
| TLE error growth | Levit & Marshall, Improved orbit predictions using two-line elements (Adv. Space Res. 47(7), 2011) |
The algorithmic choices were checked against authoritative operational practice (US 18/19 SDS, NASA CARA, ESA):
- Pc method — the Foster (1992) 2-D collision-plane integral is
the operational standard (the CCSDS CDM literally encodes
COLLISION_PROBABILITY_METHOD = FOSTER-1992) and agrees with the Chan / Patera / Alfano methods to ≥ 2 significant figures. - Combining — combined covariance is the term-by-term sum of the two objects' covariances; combined HBR is the sum of the two radii (the "supervening sphere"), and Pc scales with the square of HBR.
- Decision thresholds — the engine classifies risk on
Pc ≥ 1e-4(critical),Pc ≥ 1e-6(warning) andPc ≥ 1e-8(watch), each paired with a miss-distance floor (Conjunction_Analysis.Classify). The critical threshold matches 18 SDS / NASA CARA practice (whose precise red value is 4.4e-4) and ESA (1e-5–1e-4); miss distance is a joint triage criterion (near-Earth ≤ 1 km, deep-space ≤ 5 km). - Hard-body radius — when the true size is unknown we screen with a per-object-type bounding radius (rocket bodies 8 m, else 5 m). This is a CARA-style modeling choice (CARA uses a static secondary HBR sized to bound ~95 % of secondaries), not an 18 SDS standard — 18 SDS uses RCS or an operator-supplied HBR.
- Validity regime (important) — Foster 2-D assumes a hyperkinetic
(high relative velocity), short, well-defined encounter with a
Gaussian, constant covariance. Events that violate this — low
relative velocity (slow/co-orbiting, no well-defined TCA) or aged
covariance — are surfaced via a per-event
pc_confidenceflag (nominal/low_rel_velocity/aged_covariance) and, following NASA CARA, cross-checked with a curved-dynamics Monte-Carlo Pc (pc_mc, see Monte-Carlo Pc cross-check); the 2-D Pc bias there is not guaranteed conservative.
Sources: 18/19 SDS Spaceflight Safety Handbook for Operators v1.7; NASA CARA (AAS 19-668, AAS 19-632); Alfano, Review of Conjunction Probability Methods for Short-Term Encounters; ESA (García-Pelayo).
The numerical core is structured for static proof. The following
contracts are encoded in package specifications — see Proof status
for exactly how much of this gnatprove currently discharges:
Vector_Math.NormandNorm_Squaredare non-negative.Vector_Math.Safe_Atan2's postcondition bounds the range so no downstream domain error is possible, including on NaN input.Time_Utils.Date_To_JDis monotonically increasing on the post-1900 era and usesReal'Floorso the day-of-month coefficient cannot drift by one (a Meeus algorithm pitfall).SGP4_Propagator.Propagateeither returns OK with a finite state vector or OK = False (no exceptions cross the package boundary).
Collision_Probability (Foster's method, Monte-Carlo) is
SPARK_Mode => Off at the package level — Compute_Pc's
Result in 0.0 .. 1.0 postcondition is a real Ada contract, checked at
every call in a debug/-gnata build, but outside SPARK's analysis
boundary entirely, unlike the packages above.
The HTTP and tasking layers are intentionally SPARK_Mode => Off.
SPARK does not analyse GNAT.Sockets, Ada.Calendar or unbounded
strings, so we partition those surfaces and treat them as the
trusted boundary.
Correctness of the propagator is checked against the canonical Vallado
reference output (tcppver.out from Revisiting Spacetrack Report #3,
AIAA 2006) for object 00005:
gprbuild -P tests/tests.gpr
./tests/bin/sgp4_verify # near-Earth SGP4 vs Vallado tcppver.out
./tests/bin/sdp4_verify # deep-space SDP4 vs satellite.jsThe same reference vectors were independently reproduced by the
frontend's satellite.js propagator to 6 nm – 7 mm at t = 0, 360
and 720 minutes — so the reference data and the live-mode propagation
path are confirmed correct, and the Ada test asserts the backend port
matches them.
Deep-space (SDP4) correctness is asserted directly against the
live-mode engine: sdp4_verify propagates a geostationary object
(synchronous resonance, irez=1), a GPS/MEO object (non-resonant deep
space, irez=0) and a Molniya object (half-day resonance, irez=2)
out to 48 h and compares the Ada state against
satellite.js sgp4(satrec, tsince) — the exact routine the browser
runs. Every case matches to below 1 m / 1 mm·s⁻¹ (in fact below
the test's print precision), confirming deep-space live/backend parity.
Proof status: gnatprove runs cleanly against this project — via a
Linux container, since Windows' Smart App Control blocks the local
toolchain — and proves every check it currently analyses: 3 of 3,
all trivial index-bounds checks on the Identity_Matrix constant in
Orbital_Types. That number is small because Vector_Math,
Time_Utils and SGP4_Propagator carry SPARK_Mode => On
specifications with the contracts above, but SPARK_Mode => Off
bodies — they call Ada.Numerics elementary functions (sqrt, trig)
outside the analysable subset — so gnatprove structurally skips every
Pre/Post contract in those three packages rather than failing to prove
it; Collision_Probability disables SPARK_Mode for the whole package,
so none of its contracts are even candidates. The contracts are real
Ada assertions (checked at every call in a debug/-gnata build) and
checkable in principle at the interface, but almost none of the
numerical core has actually been discharged by the prover yet — this is
contract-annotated and analysable, not yet a stamped proof, and
today's real number is smaller than that phrase might suggest.
Roughly half of Vector_Math and Time_Utils's subprograms (Dot,
Cross, the vector operators, Date_To_JD, GMST, Minutes_Between,
…) are pure Real arithmetic with no transcendental calls, so
narrowing the SPARK_Mode => Off boundary to wrap only the actual
Ada.Numerics calls would let gnatprove discharge real
postconditions on them without needing to axiomatise sqrt/sin/cos — a
tractable next step this codebase has not yet taken. Run-time safety
holds regardless of proof status: every body is exception-guarded so a
fault degrades to OK => False rather than crashing.
- The propagator runs both SGP4 (near-Earth) and SDP4 (deep-space). Objects with period ≥ 225 minutes (GEO, GTO, GPS, Molniya) are propagated through the deep-space luni-solar + resonance model and are included in screening alongside LEO objects.
- Covariance is synthesised from TLE epoch age, not loaded from
CDMs (Conjunction Data Messages); real operational use would ingest
CCSDS-formatted CDMs via the same HTTP layer. The synthesis is anchored
to measured LEO TLE accuracy — along-track 1-σ ≈ 0.8 km at epoch growing
≈ 1.5 km/day (Levit & Marshall 2011), with smaller radial / cross-track
components (Flohrer, Krag & Klinkrad 2008) — but is still a population
average, not a per-object OD covariance, so it is not guaranteed
conservative. Every event therefore carries a
pc_confidenceflag and slow / aged encounters are cross-checked with a curved-dynamics Monte-Carlo Pc (see Monte-Carlo Pc cross-check). - The within-catalog screen uses a spatial pre-filter: every object
is propagated onto a shared coarse time grid once (O(N·steps) — not
O(N²·steps) — propagations); each coarse step is then treated as a
segment, and candidate pairs are found from the closest approach of
the two objects' linearly interpolated positions across that
segment (not just the sampled endpoints), so a fast crossing cannot
hide between two samples. A per-step sweep-and-prune on the x-axis
keeps this from degrading to an all-pairs scan. Surviving candidates
are golden-section TCA-refined and Foster-Pc'd, and every distinct
contiguous run of qualifying segments becomes its own event, so two
unrelated close approaches of the same pair in one window are both
reported. It is verified to return exactly the same conjunctions as
the un-pruned O(N²) reference and to scale sub-quadratically on a
Fengyun-scale (~3500-object) cloud (
tests/screen_verify) — no fixed per-cycle timing figure is asserted, since it depends on catalog density and hardware. When more close approaches are found than the event cap, the most dangerous (highest Pc, then smallest miss) are retained. - The maneuver planner uses linear CW dynamics, valid while the chief orbit is near-circular (e ≲ 0.01) and the burn-to-TCA separation stays small relative to the orbital radius (≲ 1 % is the well-resolved regime, degrading quadratically beyond it) — comfortably true for a single short-horizon collision-avoidance burn sized hours before a predicted close approach, which is what this planner does. A multi-orbit rendezvous or an eccentric-chief scenario would need the Tschauner-Hempel/Yamanaka-Ankersen linear generalisation or, beyond that, a full Lambert / pseudospectral solver — neither of which this planner implements or needs for CAM sizing.
This project is released under the MIT license. NASA imagery is in the public domain (NASA copyright policy: https://www.nasa.gov/multimedia/guidelines/index.html). TLE data from Celestrak is freely redistributable per their terms of use.