Skip to content

AGENTS.md

Latest commit

 

History

History
128 lines (105 loc) · 6.83 KB

AGENTS.md

File metadata and controls

128 lines (105 loc) · 6.83 KB

AGENTS.md — Rivet Project Instructions

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

Project Overview

This project uses Rivet for SDLC artifact traceability.

  • Config: rivet.yaml
  • Schemas: common, aspice, gale
  • Artifacts: 755 across 11 types
  • Validation: rivet validate (current status: 16 errors)

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
finding 2 Research finding or gap analysis result that may generate requirements or inform design decisions. Not part of the ASPICE V-model — tracked separately for audit trail and decision rationale.
source-provenance 34 Pins an upstream source file being replaced. Records the exact file path, version, checksum, and the corresponding Gale Rust file that replaces it. This is the root of the traceability chain — every requirement ultimately traces back to a provenance record proving what original code is replaced.
stakeholder-req 105 Stakeholder requirement (SYS.1)
sw-arch-component 39 Software architectural element (SWE.2)
sw-detail-design 98 Software detailed design or unit specification (SWE.3)
sw-integration-verification 35 Software component and integration verification measure (SWE.5 — Software Component Verification and Integration Verification)
sw-req 252 Software requirement (SWE.1)
sw-verification 85 Software verification measure against SW requirements (SWE.6 — Software Verification)
sys-verification 10 System verification measure against system requirements (SYS.5 — System Verification)
system-req 37 System requirement derived from stakeholder needs (SYS.2)
unit-verification 58 Unit verification measure (SWE.4 — Software Unit Verification)
documentation 0 Upstream document structure (sections, text blocks) imported from ReqIF. Not requirements — kept for context and traceability completeness.
sys-integration-verification 0 System integration and integration verification measure (SYS.4 — System Integration and Integration Verification)
system-arch-component 0 System architectural element (SYS.3)
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
  • 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
allocated-to Source is allocated to the target (e.g. requirement to architecture component) allocated-from
constrained-by Source is constrained by the target constrains
derives-from Source is derived from the target derived-into
function-maps-to A detailed design element maps to a specific C function in the upstream source. Used for line-level traceability.
function-mapped-from
generates A finding generates a derived requirement. Indicates the requirement was created as a result of the finding.
generated-by
implements Source implements the target implemented-by
informs A finding or analysis informs a requirement or design decision. Non-normative link for rationale traceability.
informed-by
mitigates Source mitigates or prevents the target mitigated-by
part-of-execution Verification verdict belongs to a verification execution run contains-verdict
refines Source is a refinement or decomposition of the target refined-by
related-to General association between artifacts. Used when the relationship is informational rather than structural.
related-to
replaces Gale artifact replaces the upstream source identified by the target provenance record. This is the fundamental porting relationship.
replaced-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

Formal Verification

This project uses triple-track formal verification. Follow the PulseEngine Formal Verification Guide for all proof work.

Key rules:

  • Code must satisfy all verification tracks simultaneously (Verus, Rocq, Kani)
  • Write to the intersection: no trait objects, no closures, no async in verified code
  • verus-strip bridges Verus-annotated source to plain Rust for other tools
  • Get the spec right before attempting proofs
  • Try the simple thing first — let the solver attempt it before adding manual steps
  • Bazel rules: rules_verus, rules_rocq_rust, rules_lean

Running verification locally

# Verus SMT (requires Nix)
nix develop --command bazel test //:verus_test

# Kani BMC
nix develop --command bazel test //:kani_test //:kani_ffi_test

# Rocq proofs
nix develop --command bazel test //proofs:all

# Lean proofs
nix develop --command bazel test //proofs/lean:all

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