Assurance Case — Project VELA

What this is. A GSN-style (Goal Structuring Notation), AMLAS-informed safety argument for VELA’s readiness to be reviewed by a space-agency review board (ISRO / ESA) as a starting assurance case. It states an explicit top claim, decomposes it into sub-claims, and ties each sub-claim to concrete evidence that exists in this repository today — every cited path was verified before inclusion. Where evidence does not yet exist, it is named honestly in §5 (“Assurance gaps”). This is a living argument, not a certification; it confers no compliance status and is our own reasoned position, not an external determination.

Owner: SKOPAQ AI Pvt Ltd. Proprietary. Scope: VELA v1 — ground-segment, advisory-only anomaly-investigation co-pilot.

Sibling documents (read alongside this case): docs/assurance/classification-and-safety-case.md (software classification, NPR 7150.2 Class-E argument), docs/assurance/hazard-analysis.md, docs/assurance/rtm.csv (requirements traceability), docs/policies/incident-response-citation-integrity.md, CLAUDE.md (the hard guardrails), docs/design/02-ARCHITECTURE.md.

1. GSN vocabulary used here

Symbol	GSN element	Meaning in this document
G	Goal	A claim to be shown true.
S	Strategy	The argument approach that decomposes a goal into sub-goals.
Sn	Solution	The evidence (a file, a test, a CI job) that discharges a goal.
A	Assumption	A stated premise the argument relies on.
C	Context	Scoping information for a goal or strategy.
J	Justification	Why a strategy is adequate.

Convention below: a Solution node names the real artifact and, where the artifact is a test, the test function or CI step that exercises it. A Solution is only cited if the underlying file exists in the tree.

2. Top-level argument (overview)

G0 (Top claim). VELA is a safe, advisory-only, ground-segment anomaly-investigation co-pilot: it turns a telemetry deviation into a cited root-cause narrative and a drafted recovery procedure that a human reviews, and it cannot — by construction — be the proximate cause of a spacecraft action.

C0 (Context). VELA runs in the operations centre, never onboard. Its only output is a recommendation to a human. See docs/assurance/classification-and-safety-case.md §1.

A0 (Assumption). The operator and the commanding chain are outside VELA’s boundary and unchanged by it. VELA’s failure effect is mediated entirely by that human. This assumption is the load-bearing premise of the whole case; if it were violated (i.e. VELA gained a command path), the classification argument would collapse and G1 becomes the first line of defence.

S0 (Strategy). Argue over the distinct mechanisms by which an advisory co-pilot could still do harm, and show each is closed by a control with in-repo evidence. J: these six sub-goals map one-to-one onto CLAUDE.md’s hard guardrails (#1 commanding, #2 fabrication, #3 citations, #4 MCP boundary, #5 both modes, #6 determinism), which are the project’s own stated safety invariants.

3. Sub-claims and evidence

G1 — No commanding surface exists (advisory-only is enforced, not merely intended)

Strategy S1. Show that command issuance is impossible to introduce silently: a grep-level invariant blocks issuance identifiers at three independent choke points (developer machine + two CI workflows), while deliberately permitting read-only command history and the telecommand context filter, which are core features.

Node	Evidence in repo
Sn1.1	`scripts/guardrails/no-commanding.sh` — greps `apps/` and `vela/` for issuance-only identifiers (`issueCommand`, `send_command`, `transmit_command`, `CommandingApi`, `/api/**/commands`, …). Exit 1 on any match.
Sn1.2	`.husky/pre-commit` runs the script on every commit (pre-commit hook, `bash scripts/guardrails/no-commanding.sh`).
Sn1.3	`.github/workflows/python-ci.yml` step “No-commanding guardrail”, and `.github/workflows/security.yml` job `guardrails` step “No-commanding guardrail (audit invariant #3)” — the check runs in two separate CI workflows, so disabling one does not disable the invariant.
Sn1.4	Architectural: `vela/agents/` may import only `vela.mcp.client` for data; the MCP tool surface (`vela/mcp/client.py`) exposes no command-issuance tool. Enforced by import-linter (`[tool.importlinter]` in `pyproject.toml`, `type = "forbidden"`).

A1. The identifier pattern is a necessary-not-sufficient net: it catches the known issuance idioms. A novel idiom that matches none of the patterns would pass — see §5 gap on this. This is honestly a lexical guard, not a proof of the absence of a command path; its strength is that it is cheap, always-on, and triples up across hooks and CI.

G2 — No hallucinated citation can be released (citation integrity)

Strategy S2. Every narrative/procedure claim carries Citation objects; a single deterministic choke point verifies each citation resolves against the KG/doc store, and the rule is symmetric and both halves enforced: a grounded step with no citation is a violation, and an UNGROUNDED step that carries a citation is also a violation. The check returns two distinct booleans — ok (integrity holds) and releasable (ok and no ungrounded steps) — so a truthful “I don’t know” (UNGROUNDED) never masquerades as grounded, and it blocks release rather than failing integrity.

Node	Evidence in repo
Sn2.1	`vela/audit/citation_check.py` — `check_citations(report, client) -> CitationCheckResult(ok, releasable, checked, violations)`. It is the single choke point every entry point (CLI, API, eval) routes through; the outcome is recorded (observability) so a sev-1 integrity failure can never be silent.
Sn2.2	Adversarial hallucination suite — `tests/unit/test_citation_check.py`: `test_fabricated_ref_rejected` (a `DOC` ref to `eps_manual:does-not-exist#9.9` fails `ok`), `test_tampered_sha256_rejected`, `test_wrong_section_excerpt_rejected`, `test_homoglyph_docid_rejected` (a look-alike Unicode doc id is rejected), and `test_kg_citation_to_missing_node_rejected`. These are the “attacker forged a plausible-looking reference” cases.
Sn2.3	The `ok` / `releasable` distinction is pinned by `test_ungrounded_step_passes_integrity_but_blocks_release` (integrity holds, `releasable == False`) and `test_ungrounded_step_carrying_citation_is_a_violation` (the reverse asymmetry). `test_grounded_step_without_citation_rejected` closes the other half.
Sn2.4	Policy: a hallucinated reference is a sev-1 with a defined response — `docs/policies/incident-response-citation-integrity.md`.
Sn2.5	Operational consequence: `python -m vela.cli investigate` exits 1 on a citation-integrity violation, so a hallucination fails a pipeline rather than shipping.

C2. “Resolves” means the reference maps to a real node/section in VELA-REF-1 (vela/kg/reference/reference_graph.py) or the seeded doc store — not to an external truth. G2 proves provenance integrity, not factual correctness of the source; the latter is a data-curation concern, not a software-integrity one.

G3 — The release gate is fail-closed and model-independent

Strategy S3. Show that a high-severity or ungrounded draft cannot auto-release regardless of which reasoning model produced it, by placing the withhold gate in deterministic graph code that every model path traverses, and by pinning the eval on releasable matching expectation.

Node	Evidence in repo
Sn3.1	`vela/agents/nodes.py::drafter_node` appends `_escalation_step(...)` — a deliberately UNGROUNDED escalation step that sets `releasable=False` — for all models. The code comment records the history: this used to live in the deterministic model only, which the LLM path bypassed (the `releasable_match` gap); it was moved so “the LLM path cannot bypass it and over-release a high-severity draft.”
Sn3.2	`vela/agents/models/deterministic.py` — the escalation withhold-gate is explicitly no longer added in the model, with a NOTE pointing to `drafter_node` as the single source. This is the concrete fix for model-independence.
Sn3.3	`vela/agents/nodes.py::approval_node` computes `requires_review = any(s.ungrounded or s.risk_level == HIGH for s in steps)` — an ungrounded or high-risk step forces the human-review flag.
Sn3.4	Fail-closed degradation target: `drafter_node` produces an `INSUFFICIENT` verdict with no cited claim and no procedure on an LLM `ReasoningError` (see `_degraded_*` helpers in `vela/agents/nodes.py`) — an infra failure yields a non-releasable “escalate” result, never a confident uncited answer.
Sn3.5	The eval scores `releasable` against expectation, not just the verdict — `vela/eval/scoring.py` computes `releasable_match = raw.releasable == exp.releasable` and reports `releasable_match_rate` (`vela/eval/schema.py`, `vela/eval/compare.py`). `tests/unit/test_anthropic_model.py` pins that the LLM path no longer over-releases (the `releasable_match` fix).

J3. Putting the gate in drafter_node (deterministic graph structure) rather than in a model makes the safety property hold by construction across models: adding a new reasoning backend cannot regress it without editing the shared node, which is covered by the eval.

G4 — Investigations are deterministic and reproducible

Strategy S4. Argue that LLM judgment sits on top of deterministic scaffolding, never instead of it: graph traversal, event forming, citation checking, and replay are deterministic and seeded, with as_of fixed, and a golden test asserts bit-for-bit reproducibility of verdict, citations, procedure steps, and hypothesis ranking.

Node	Evidence in repo
Sn4.1	`vela/agents/models/deterministic.py` — `DeterministicModel`, the default and the model required in `airgap` mode. `airgap` hard-fails if `reasoning != "deterministic"` (`vela/config.py`), so the reproducible path is not optional in the offline posture.
Sn4.2	`tests/golden/test_end_to_end.py::test_deterministic_reproducibility` — two runs of `CELL_DEGRADATION` must agree on verdict, on the ordered list of citation refs, on procedure-step text, and on ranked-hypothesis `(fm_code, status, support_score)` tuples.
Sn4.3	Both modes are exercised: `tests/conftest.py` parametrizes the `mode` fixture over `("airgap", "cloud")`, so every golden case runs twice; `test_report_carries_the_mode_it_ran_in` guards that the parametrization really drives both.
Sn4.4	Ranking is deterministic and not guessed: `test_competing_failure_modes_are_ranked_not_guessed` shows two EPS failure modes claiming `battery_temp` resolve deterministically (thermal precursor vs capacity fade).
Sn4.5	Checkpointed forensic replay: `vela/agents/graph.py` compiles with a `MemorySaver` checkpointer keyed by `thread_id == investigation_id`; `graph.get_state_history()` yields the run’s replay sequence — one investigation, one auditable record.

A4. Reproducibility is guaranteed for the deterministic path (the CI/golden path). The real-Claude path (AnthropicModel) is not bit-reproducible and is not claimed to be — see §5.

G5 — Asserted values are grounded (telemetry-value gate + entailment gate)

Strategy S5. Close the gap that citation-resolution alone leaves — a citation can resolve perfectly yet the sentence around it can invent a number or point at an off-topic span — with two additive gates, both selectable by config and both with honest documented limits.

Node	Evidence in repo
Sn5.1	Gate 1 — telemetry-value grounding: `vela/audit/telemetry_grounding.py::check_telemetry_grounding`. Extracts numeric assertions from narrative/procedure prose and flags any that trace to neither a telemetry value returned this run nor a number verbatim in a retrieved knowledge source. Deterministic, no LLM. Unit-tested in `tests/unit/test_telemetry_grounding.py`.
Sn5.2	Gate 2 — citation entailment: `vela/audit/entailment.py::check_entailment`. `LexicalOverlapEntailment` is the deterministic offline floor (catches an off-topic span); `NLIEntailmentChecker` is the real semantic backend (local cross-encoder, `nli` extra) that catches on-topic-but-unsupported phrasing the lexical floor cannot see. Selected by config like `DocSearch`. Unit-tested in `tests/unit/test_entailment.py`.
Sn5.3	Both gates are proven to run through the production wiring (not just in isolation): `tests/integration/test_grounding_gates_e2e.py::test_both_gates_pass_on_deterministic_investigation` asserts the pipeline captures a `GroundingRecord` and both gates pass on a real deterministic investigation.

A5 (honest scope, taken verbatim from the module docstrings). Gate 1 catches an invented value; it does not catch a real value misattributed to the wrong channel, nor a fabricated value that coincidentally equals a retrieved number. Gate 2’s lexical floor catches a topically-unrelated span but does not catch an on-topic-but-wrong claim (that is Gate 1’s job) and misses genuine paraphrase (which the NLI backend reads). Each gate is a floor, not a proof; together they are defence-in-depth under the LLM path, layered beneath G2.

G6 — A human approves before any release (human-in-the-loop is graph structure)

Strategy S6. Show that approval is enforced by the control-flow graph itself — a real interrupt() — not by a UI convention that a caller could skip.

Node	Evidence in repo
Sn6.1	`vela/agents/nodes.py::approval_node` calls LangGraph `interrupt(...)`; the drafter pauses and no procedure draft is released until the node resumes with an explicit decision (`Command(resume={"approved": ..., "approved_by": ...})`).
Sn6.2	`vela/agents/graph.py` compiles the graph with a `MemorySaver` checkpointer keyed on `investigation_id`; the interrupt/resume is exercised end-to-end by `tests/integration/test_approval_gate.py`.
Sn6.3	Safety-critical idempotency is documented and honoured: on resume LangGraph re-executes `approval_node` from the top, so everything before `interrupt()` is deterministic, side-effect-free state reads only — the code comment in `approval_node` states this invariant explicitly, protecting against a non-deterministic double-execution on resume.
Sn6.4	The released decision is stamped into the audit log (`approved_by`, “released (approved by …)” / “held pending approval”) via the `audit_log` reducer, so the approver is part of the forensic record.

A6. MemorySaver is process-local: the two-request release only holds within one server process and checkpoints do not survive a restart. For multi-process production this must become a durable (SQLite/Postgres) checkpointer — see §5. The safety property (no release without an explicit decision) holds within a process today; the durability of the gate across processes does not yet.

4. Assurance-invariant → evidence traceability

#	CLAUDE.md hard guardrail	Sub-goal	Primary evidence (verified path)
1	No commanding	G1	`scripts/guardrails/no-commanding.sh`, `.husky/pre-commit`, `python-ci.yml`, `security.yml`
2	No fabricated data	G2 (data), C0	`vela/kg/reference/reference_graph.py`, `vela/adapters/replay/` (synthetic-only)
3	Citations load-bearing	G2	`vela/audit/citation_check.py`, `tests/unit/test_citation_check.py`
4	Agents reach data only via MCP	G1, G3	`pyproject.toml [tool.importlinter]`, `vela/mcp/client.py`
5	Both modes must pass	G4	`tests/conftest.py` mode fixture, `python-ci.yml` both-mode smoke
6	Determinism where possible	G4	`tests/golden/test_end_to_end.py::test_deterministic_reproducibility`
—	Fail-closed release, model-independent	G3	`vela/agents/nodes.py::drafter_node` / `approval_node`, `vela/eval/scoring.py`
—	Grounding gates	G5	`vela/audit/telemetry_grounding.py`, `vela/audit/entailment.py`, `tests/integration/test_grounding_gates_e2e.py`
—	Human-in-the-loop	G6	`vela/agents/nodes.py::approval_node`, `tests/integration/test_approval_gate.py`

The machine-readable requirements trace is docs/assurance/rtm.csv; the classification argument that sits above this case is docs/assurance/classification-and-safety-case.md.

5. Assurance gaps — not yet evidenced (read this before trusting the case)

An assurance case is only credible if it is candid about what it does not yet show. The following are stated as open items, not hidden:

Single mission / single reference spacecraft. All evidence is against one synthetic reference spacecraft (VELA-REF-1) and ten seeded replay scenarios. There is no evidence of generality across real missions, real telemetry irregularity at scale, or a second spacecraft’s KG. The case demonstrates the controls work, not that the product generalises.
The LLM path is not gated through the graph in CI. AnthropicModel (vela/agents/models/anthropic.py) is implemented and live-verified and its release-blocking grounding gates fail closed to INSUFFICIENT — but it is not exercised through the full graph in the CI/golden suite. Cloud mode is a deployment posture with a real-but-untested-in-suite LLM path. G3/G5 protect it by construction, but there is no continuous end-to-end LLM regression evidence yet. This is the single most important gap for a review board.
Fault injection stops above the adapter layer. The adversarial tests target the citation and grounding checkers with forged references and invented numbers (G2, G5). There is no systematic fault-injection at the telemetry-adapter / replay boundary — corrupted, truncated, or out-of-order telemetry frames, clock skew, or a store returning malformed rows are not yet fuzzed. Robustness to malformed inputs is asserted by design intent, not by a fault-injection suite.
No formal verification. Every safety property here is argued by test + deterministic code review + always-on lint/grep, not by formal methods (model checking, theorem proving, or a proven information-flow analysis of the no-command property). The no-commanding guard (Sn1.1) is a lexical net that catches known issuance idioms; it is not a proof that no command path can exist. A determined refactor using an unlisted identifier would evade it until the pattern is extended.
Approval durability is process-local. Per A6, the human-in-the-loop gate relies on a process-local MemorySaver; a production deployment needs a durable checkpointer before the approval gate is trustworthy across restarts and multiple server processes.
Coverage is uneven by design. audit/, detection/, kg/ target ≥ 90% and MCP servers ≥ 80% (contract tests), but the agent layer is eval-gated by golden cases, not line-gated (CONTRIBUTING.md). A review board should read the golden suite, not a coverage number, as the agent-layer evidence.

6. How to reproduce the evidence

A reviewer can regenerate every Solution node above from a clean checkout:

make check          # ruff + mypy --strict + import-linter + no-commanding + pytest (THE gate)
make guardrail      # G1  — scripts/guardrails/no-commanding.sh alone
.venv/bin/python -m pytest tests/unit/test_citation_check.py -q          # G2 adversarial suite
.venv/bin/python -m pytest tests/integration/test_grounding_gates_e2e.py -q  # G5 both gates
.venv/bin/python -m pytest tests/integration/test_approval_gate.py -q    # G6 interrupt/resume
.venv/bin/python -m pytest tests/golden/test_end_to_end.py \
  -k "reproducibility or ranked" -q                                      # G4 determinism
make eval           # golden cases, both modes (G3 releasable_match, G4)

CI runs the same gate on every push: .github/workflows/python-ci.yml (ruff · mypy · import-linter · no-commanding · pytest · both-mode end-to-end smoke) and .github/workflows/security.yml (the guardrails job).

This document is a starting assurance case offered in good faith for review. It is not a certification, makes no claim of external accreditation, and names its own gaps in §5. Corrections and challenges from a review board are expected and welcome.