AGENTS.md

NOTE: This section is auto-generated by rivet init --agents. Do not edit between the BEGIN rivet-managed / END rivet-managed markers — edits there are overwritten on regeneration. Content outside the markers is preserved.

AGENTS.md — Rivet Project Instructions

This section was generated by rivet init --agents. Re-run the command any time artifacts change to keep it current.

Project Overview

This project uses Rivet for SDLC artifact traceability.

• Config: rivet.yaml
• Schemas: common, dev, aspice, stpa, aadl, sysml2
• Artifacts: 666 across 12 types
• Validation: rivet validate (current status: pass)

Available Commands

Command	Purpose	Example
rivet validate	Check link integrity, coverage, required fields	rivet validate --format json
rivet list	List artifacts with filters	rivet list --type requirement --format json
rivet stats	Show artifact counts by type	rivet stats --format json
rivet add	Create a new artifact	rivet add -t requirement --title "..." --link "satisfies:SC-1"
rivet link	Add a link between artifacts	rivet link SOURCE -t satisfies --target TARGET
rivet serve	Start the dashboard	rivet serve --port 3000
rivet export	Generate HTML reports	rivet export --format html --output ./dist
rivet impact	Show change impact	rivet impact --since HEAD~1
rivet coverage	Show traceability coverage	rivet coverage --format json
rivet diff	Compare artifact versions	rivet diff --base path/old --head path/new

Artifact Types

Type	Count	Description
control-action	21	An action issued by a controller to a controlled process or another controller.
controlled-process	10	A process being controlled — the physical or data transformation acted upon by controllers.
controller	22	A system component (human or automated) responsible for issuing control actions. Each controller has a process model — its internal beliefs about the state of the controlled process.
controller-constraint	47	A constraint on a controller's behavior derived by inverting a UCA. Specifies what the controller must or must not do.
design-decision	76	An architectural or design decision with rationale
feature	139	A user-visible capability or feature
hazard	32	A system state or set of conditions that, together with worst-case environmental conditions, will lead to a loss.
loss	19	An undesired or unplanned event involving something of value to stakeholders. Losses define what the analysis aims to prevent.
loss-scenario	36	A causal pathway describing how a UCA could occur or how the control action could be improperly executed, leading to a hazard.
requirement	183	A functional or non-functional requirement
system-constraint	24	A condition or behavior that must be satisfied to prevent a hazard. Each constraint is the inversion of a hazard.
uca	57	An Unsafe Control Action — a control action that, in a particular context and worst-case environment, leads to a hazard. Four types (provably complete): 1. Not providing the control action leads to a hazard 2. Providing the control action leads to a hazard 3. Providing too early, too late, or in the wrong order 4. Control action stopped too soon or applied too long
aadl-analysis-result	0	Output of a spar analysis pass
aadl-component	0	AADL component type or implementation imported from spar
aadl-flow	0	End-to-end flow with latency bounds
aadl-tool	0	An AADL ecosystem tool — captures what it does, what makes it unique, and what capabilities spar could adopt from it.
stakeholder-req	0	Stakeholder requirement (SYS.1)
sub-hazard	0	A refinement of a hazard into a more specific unsafe condition.
sw-arch-component	0	Software architectural element (SWE.2)
sw-detail-design	0	Software detailed design or unit specification (SWE.3)
sw-integration-verification	0	Software component and integration verification measure (SWE.5 — Software Component Verification and Integration Verification)
sw-req	0	Software requirement (SWE.1)
sw-verification	0	Software verification measure against SW requirements (SWE.6 — Software Verification)
sys-integration-verification	0	System integration and integration verification measure (SYS.4 — System Integration and Integration Verification)
sys-verification	0	System verification measure against system requirements (SYS.5 — System Verification)
sysml-action	0	SysML v2 action definition (behavioral)
sysml-component	0	SysML v2 part definition or usage
sysml-interface	0	SysML v2 interface or port definition
sysml-requirement	0	SysML v2 requirement (def or usage)
system-arch-component	0	System architectural element (SYS.3)
system-req	0	System requirement derived from stakeholder needs (SYS.2)
unit-verification	0	Unit verification measure (SWE.4 — Software Unit Verification)
verification-execution	0	A verification execution run against a specific version
verification-verdict	0	Pass/fail verdict for a single verification measure in an execution run

Working with Artifacts

File Structure

• Artifacts are stored as YAML files in: artifacts, safety/stpa, safety/stpa/requirements.yaml, safety/stpa/architecture.yaml, safety/stpa/validation.yaml, safety/stpa/solver-requirements.yaml
• Schema definitions: schemas/ directory
• Documents: docs

Creating Artifacts

rivet add -t requirement --title "New requirement" --status draft --link "satisfies:SC-1"

Validating Changes

Always run rivet validate after modifying artifact YAML files. Use rivet validate --format json for machine-readable output.

Link Types

Link Type	Description	Inverse
acts-on	Control action acts on a process or controller	acted-on-by
allocated-from	Component is allocated from (traces back to) a requirement or architecture element	allocated-to
allocated-to	Source is allocated to the target (e.g. requirement to architecture component)	allocated-from
caused-by-uca	Loss scenario is caused by an unsafe control action	causes-scenario
constrained-by	Source is constrained by the target	constrains
constrains-controller	Constraint applies to a specific controller	controller-constrained-by
constraint-satisfies	Requirement satisfies (implements) a system constraint	satisfied-by-constraint
contains	Parent AADL component contains a child sub-component	contained-by
depends-on	Source depends on target being completed first	depended-on-by
derives-from	Source is derived from the target	derived-into
implements	Source implements the target	implemented-by
inverts-uca	Controller constraint inverts (is derived from) an UCA	inverted-by
issued-by	Control action or UCA is issued by a controller	issues
leads-to-hazard	UCA or loss scenario leads to a hazard	hazard-caused-by
leads-to-loss	Hazard leads to a specific loss	loss-caused-by
mitigates	Source mitigates or prevents the target	mitigated-by
modeled-by	An architecture component is modeled by an AADL component	models
part-of-execution	Verification verdict belongs to a verification execution run	contains-verdict
prevents	Constraint prevents a hazard	prevented-by
refines	Source is a refinement or decomposition of the target	refined-by
result-of	Verification verdict is the result of executing a verification measure	has-result
satisfies	Source satisfies or fulfils the target	satisfied-by
traces-to	General traceability link between any two artifacts	traced-from
verifies	Source verifies or validates the target	verified-by

Conventions

• Artifact IDs follow the pattern: PREFIX-NNN (e.g., REQ-001, FEAT-042)
• Use rivet add to create artifacts (auto-generates next ID)
• Always include traceability links when creating artifacts
• Run rivet validate before committing

Spar contributor quick map

Spar-specific guidance for contributors and agents (outside the rivet-managed section above):

• Build: cargo build --workspace. Single-binary CLI: cargo build --release -p spar.
• Tests: cargo test --workspace. Per-crate fixtures live under each crate's tests/ directory.
• Salsa graph: query definitions and the incremental DB live in crates/spar-base-db/; HIR-side queries are in crates/spar-hir-def/ and crates/spar-hir/. Add new queries near existing ones — do not stand up a parallel database.
• Analysis registry: pluggable passes are wired in crates/spar-analysis/src/lib.rs (see Runner::register / register_all). New passes implement the Analysis trait and are registered there.
• Lean proofs gate: proofs live in proofs/Proofs/ (Scheduling, Network). CI runs lake build; sorry-free is required for the verified-core modules (RTA, RTAJittered, EDF, RMBound).
• Sample models: test-data/vehicle.aadl + test-data/sensor_lib.aadl are the canonical pair used in docs and smoke tests.
• Quickstart: see docs/quickstart.md for the user-facing entry point.