Tutorial: a requirements-first thermostat¶

The repository’s examples/thermostat is a deliberately small product developed the way this tool intends: user needs first, then requirements and a risk analysis, then code and tests that trace back to them — ending in a report that a golden test pins in review. Every requirement names the test cases that verify it, and each test case verifies exactly one requirement (One test case, one requirement). It is split into three components, one per supported test framework:

Component	Language	Hook	Requirements
`thermostat/` — controller and panel text	Python	pytest, unittest	REQ-1, 2, 4, 6, 7
`interlock/` — over-temperature cutoff	C++	googletest	REQ-5
`setpoint/` — setpoint parser	Rust	`rr::verifies!`	REQ-3, 4
panel inspection	—	signed record	REQ-7

To follow along, clone the repository and work in examples/thermostat, which is a Bazel module of its own that uses the ruleset from the checkout (local_path_override(path = "../..")).

1. User needs¶

Start from what the occupants of the room need, in their terms:

user_needs:
  - id: UN-1
    title: Keep the room at a comfortable temperature
    description: >-
      Once a target temperature is set, the room should settle near it without
      the heater cycling rapidly.
  - id: UN-2
    title: Set the target temperature in Celsius or Fahrenheit
    description: >-
      Occupants enter a target like "21.5C" or "70F" on the wall panel and can
      read back what they set.

2. Risks and their controls¶

A risk analysis asks what could go wrong and how badly (ISO 14971; see Background: the standards). Each risk names its hazard, the situation in which people are exposed to it, the harm, and an estimate of severity and likelihood — before and after control. Each mitigation is one risk control measure:

# Risk analysis (ISO 14971 §5) and risk control (§7). Each mitigation is a
# risk control measure implemented by requirements, so its effectiveness is
# verified by the same tests (§7.2).
risks:
  - id: RISK-1
    title: Room overheats
    hazard: Heater energised continuously
    hazardous_situation: >-
      A control fault or a sensor reading stuck low keeps the heater on while
      the room is occupied.
    harm: Heat stress; burns from surfaces near the heater
    severity: high
    likelihood: possible
    residual_severity: high
    residual_likelihood: rare
    residual: >-
      Two independent controls (interlock + sensor plausibility) must both
      fail. Accepted.

  - id: RISK-2
    title: Implausible setpoint accepted
    hazard: Setpoint far above comfort range
    hazardous_situation: >-
      "80" meant as °F is taken as °C, or a typo like "250C", and the
      controller drives the room towards it.
    harm: Heat stress
    severity: medium
    likelihood: likely
    residual_likelihood: unlikely

mitigations:
  - id: MIT-1
    title: Independent over-temperature protection
    type: protective
    description: >-
      A hardware-near interlock and a sensor plausibility check, each able to
      de-energise the heater on its own.
    mitigates: [RISK-1]
    implemented_by: [REQ-5, REQ-6]

  - id: MIT-2
    title: Validate setpoints at entry
    type: inherent
    description: Require an explicit unit and a bounded range for every setpoint.
    mitigates: [RISK-2]
    implemented_by: [REQ-3, REQ-4]

project.yaml sets the risk acceptability threshold used to check the residual estimates (high × rare scores 4 × 1 = 4 and medium × unlikely 3 × 2 = 6, both within 6). It also puts the model in charge of which requirement each test case verifies (attribution: model) and names the lock that pins every requirement’s set of cases (sets_lock, step 6):

# The thermostat's requirements model. Files in this directory are merged;
# this one holds project metadata and configuration, the others one entity
# kind each. Validate with `bazel test //:model_test`.
project:
  name: Thermostat
  description: >-
    A room thermostat: a Python controller, a C++ over-temperature interlock
    and a Rust setpoint parser, developed against user needs, requirements and
    a risk analysis, and traced to tests.
  software_safety_class: B  # IEC 62304 §4.3 (illustrative)

config:
  # Risk evaluation (ISO 14971 §5.5 / §7.3): score = (severity index + 1) x
  # (likelihood index + 1) on the default five-point scales. Residual risk
  # above this is flagged.
  acceptable_risk_score: 6
  # Test case ownership: the claims (`verified_by`) decide which requirement
  # a test case verifies, and tags only cross-check them. A test case
  # verifies at most one requirement.
  attribution: model
  # Every verification set's members, pinned: written by
  # `bazel run //:sets_lock_test.update`, reviewed like a golden.
  sets_lock: verification.rrlock

3. Requirements and test methods¶

Requirements say what the product must do. Some satisfy user needs; others exist because a mitigation needs them (REQ-5, REQ-6), and they trace upward through the mitigation instead. Each one also claims the test cases that verify it (verified_by): a target and the case paths it owns, literally or with * as the only wildcard — test_rejects_setpoints_outside_range[*] takes every parameter of that pytest test, Interlock::* every googletest case of the interlock suite. No two requirements may claim one case (Claims: which test cases verify an entity):

# Each requirement claims the test cases that verify it (`verified_by`): a
# literal case path, or a pattern whose only wildcard is '*'. A test case
# verifies at most one requirement, so no two requirements' claims may select
# one case (`rr validate` proves it: `shared-case`). The tags in the tests
# (`@pytest.mark.rr`, `RR_VERIFIES`, ...) only cross-check these claims, and
# verification.rrlock pins every set's members (`bazel run //:sets_lock_test.update`).
requirements:
  - id: REQ-1
    title: Heat when the room is below the setpoint band
    description: >-
      The heater shall turn on when the measured temperature is below
      setpoint - 0.5 °C.
    satisfies: [UN-1]
    modules: [thermostat]
    verified_by:
      - target: //:controller_test
        cases: ["tests.test_controller::test_heats_below_band"]

  - id: REQ-2
    title: Stop heating above the band; hold state inside it
    description: >-
      The heater shall turn off when the measured temperature is above
      setpoint + 0.5 °C, and keep its previous state inside the band
      (hysteresis), so it does not cycle rapidly.
    satisfies: [UN-1]
    modules: [thermostat]
    verified_by:
      - target: //:controller_test
        cases: ["tests.test_controller::test_stops_above_band_and_holds_inside_it"]

  - id: REQ-3
    title: Parse setpoints in °C and °F
    description: >-
      The panel shall accept "<number>C" and "<number>F" (case-insensitive,
      optional whitespace) and convert to °C.
    satisfies: [UN-2]
    modules: [setpoint]
    verified_by:
      - target: //:setpoint_test
        cases:
          - "tests::parses_celsius_and_fahrenheit"
          - "tests::requires_a_unit"

  - id: REQ-4
    title: Reject setpoints outside 5-30 °C
    description: The panel shall reject any setpoint that converts to below 5 °C or above 30 °C.
    satisfies: [UN-2]
    category: safety
    modules: [setpoint, thermostat]
    verified_by:
      - target: //:controller_test
        cases:
          - "tests.test_controller::test_rejects_setpoints_outside_range[*]"
          - "tests.test_controller::test_accepts_range_limits"
      - target: //:setpoint_test
        cases:
          - "tests::rejects_out_of_range"
          - "tests::checks_the_range_after_converting"

  - id: REQ-5
    title: Independent over-temperature cutoff
    description: >-
      The interlock shall force the heater off at or above 35 °C regardless of
      the controller, and keep it off until the temperature falls below 30 °C.
    category: safety
    method: TM-1
    modules: [interlock]
    verified_by:
      - target: //:interlock_test
        cases: ["Interlock::*"]

  - id: REQ-6
    title: Fail safe on an invalid sensor reading
    description: >-
      The controller shall turn the heater off when the reading is not a
      number or outside the sensor's -40..85 °C range.
    category: safety
    modules: [thermostat]
    verified_by:
      - target: //:controller_test
        cases: ["tests.test_controller::test_invalid_reading_turns_heater_off[*]"]

  - id: REQ-7
    title: Show the setpoint with its unit
    description: The panel shall display the active setpoint with its unit, e.g. "21.5 °C".
    satisfies: [UN-2]
    method: TM-2
    modules: [thermostat]
    verified_by:
      - target: //:display_test
        cases: ["display_test.DisplayTest::test_setpoint_shows_unit"]
      - target: record:panel_inspection
        level: inspection   # what the record provides; also when it is missing
        cases: ["inspection.TM-2::panel-shows-setpoint-unit"]

Two requirements demand more than the default simulation rigor, through test methods: the interlock must be verified software-in-the-loop, and the panel text must be signed off by inspection:

test_methods:
  - id: TM-1
    title: Interlock software-in-the-loop test
    level: sil
    procedure: >-
      Drive the interlock state machine through temperature ramps that cross
      the trip and reset thresholds, checking the heater enable at each step.
  - id: TM-2
    title: Visual inspection of the panel
    level: inspection
    procedure: A reviewer checks the rendered panel text and signs the record.

bazel test //:model_test validates all of this — the claims included: had REQ-4 also claimed tests::requires_*, it would fail with

requirements/requirements.yaml:55: error: [shared-case] REQ-4 and REQ-3 both claim cases of //:setpoint_test ('tests::requires_*' vs 'tests::requires_a_unit'), e.g. 'tests::requires_a_unit' (REQ-3 claims it at requirements/requirements.yaml:39). A test case verifies at most one requirement: narrow one selector.

The trace graph, coloured by the final verdicts:

4. Implementation, annotated¶

Code carries @rr(...) annotations naming what it implements (Source annotations):

# @rr(REQ-6): A reading the sensor cannot produce means the sensor is broken.
def plausible(reading_c: float) -> bool:
    lo, hi = SENSOR_RANGE_C
    return not math.isnan(reading_c) and lo <= reading_c <= hi


# @rr(REQ-4): Setpoints outside the comfort range are refused, whatever their source.
def check_setpoint(setpoint_c: float) -> float:
    if not MIN_SETPOINT_C <= setpoint_c <= MAX_SETPOINT_C:
        raise ValueError(f"setpoint {setpoint_c:.1f} °C is outside {MIN_SETPOINT_C:g}-{MAX_SETPOINT_C:g} °C")
    return setpoint_c


# @rr(REQ-1, REQ-2): Bang-bang control with a ±0.5 °C hysteresis band.
class Controller:
    def __init__(self, setpoint_c: float) -> None:
        self.setpoint_c = check_setpoint(setpoint_c)
        self.heater_on = False

    def update(self, reading_c: float) -> bool:
        """Feed one temperature reading; returns whether the heater should run."""
        if not plausible(reading_c):
            self.heater_on = False
        elif reading_c < self.setpoint_c - BAND_C:
            self.heater_on = True
        elif reading_c > self.setpoint_c + BAND_C:
            self.heater_on = False
        return self.heater_on

// @rr(REQ-5): Over-temperature interlock, independent of the controller.
// Trips at kTripC and stays tripped until the temperature drops below kResetC.
class Interlock {
 public:
  static constexpr double kTripC = 35.0;
  static constexpr double kResetC = 30.0;

  // Feeds a reading; returns whether the heater may be energised.
  bool HeaterAllowed(double reading_c);
  bool tripped() const { return tripped_; }

 private:
  bool tripped_ = false;
};

// @rr(REQ-3, REQ-4): Explicit unit required; the result is range-checked in °C.
pub fn parse(text: &str) -> Result<f64, Error> {
    let t = text.trim();
    let (num, unit) = t.split_at(t.len().saturating_sub(1));
    let value: f64 = num.trim().parse().map_err(|_| Error::Syntax(text.to_string()))?;
    let celsius = match unit {
        "C" | "c" => value,
        "F" | "f" => (value - 32.0) * 5.0 / 9.0,
        _ => return Err(Error::Syntax(text.to_string())),
    };
    if !(MIN_C..=MAX_C).contains(&celsius) {
        return Err(Error::OutOfRange(celsius));
    }
    Ok(celsius)
}

5. Tests, one hook per language¶

The model’s claims decide which requirement a test verifies, so a test needs no tag. Each test here still names its one requirement through its framework’s hook, as a cross-check: a tag that disagrees with the claim owning its case is a tag-mismatch gap in the report.

pytest tests use the rr marker:

@pytest.mark.rr("REQ-1")
def test_heats_below_band():
    ctl = Controller(21.0)
    assert ctl.update(20.4) is True


@pytest.mark.rr("REQ-2")
def test_stops_above_band_and_holds_inside_it():
    ctl = Controller(21.0)
    ctl.update(19.0)
    assert ctl.update(21.4) is True  # inside the band: keep heating
    assert ctl.update(21.6) is False
    assert ctl.update(20.6) is False  # inside the band: stay off

The unittest suite uses the decorator and rr.unittest_main():

class DisplayTest(unittest.TestCase):
    # Automated check of the text; the rendered panel is signed off by
    # inspection (evidence/panel_inspection.rr.yaml) as TM-2 demands.
    @rr.verifies("REQ-7")
    def test_setpoint_shows_unit(self):
        self.assertEqual(format_setpoint(21.5), "21.5 °C")
        self.assertEqual(format_setpoint(5), "5.0 °C")


if __name__ == "__main__":
    rr.unittest_main()

googletest tests call RR_VERIFIES and declare the level they provide — sil, which is what TM-1 demands of REQ-5:

TEST(Interlock, TripsAtLimit) {
  RR_VERIFIES("REQ-5");
  RR_LEVEL("sil");
  Interlock lock;
  EXPECT_TRUE(lock.HeaterAllowed(34.9));
  EXPECT_FALSE(lock.HeaterAllowed(35.0));
  EXPECT_TRUE(lock.tripped());
}

Rust tests call rr::verifies!. Until 0.3, requires_a_unit called rr::verifies!("REQ-3", "REQ-4"); a test case verifies at most one requirement, so that case was quarantined and both requirements read INVALID. Its assertions are about syntax, so it now verifies REQ-3, and the range check after converting °F, which is REQ-4’s, is a test of its own:

#[test]
fn requires_a_unit() {
    rr::verifies!("REQ-3");
    assert!(matches!(parse("21"), Err(Error::Syntax(_))));
    assert!(matches!(parse("warm"), Err(Error::Syntax(_))));
    assert!(matches!(parse(""), Err(Error::Syntax(_))));
}
#[test]
fn checks_the_range_after_converting() {
    rr::verifies!("REQ-4");
    assert!(matches!(parse("40F"), Err(Error::OutOfRange(_))));
    assert_eq!(parse("41F"), Ok(5.0));
    assert_eq!(parse("86F"), Ok(30.0));
    assert!(matches!(parse("87F"), Err(Error::OutOfRange(_))));
}

Finally, the inspection TM-2 demands is recorded as evidence in its own right (Evidence and ingestors):

# Manual verification record (TM-2). Records like this are evidence exactly
# like test results. Each is a test case of the document's `target`, which
# the model claims (REQ-7: record:panel_inspection); `requirement` names the
# one requirement it verifies, as a cross-check, and `level` the rigor it
# provides.
target: record:panel_inspection
evidence:
  - name: panel-shows-setpoint-unit
    classname: inspection.TM-2
    status: passed
    requirement: REQ-7
    level: inspection
    properties:
      procedure: TM-2
      inspector: QA reviewer
      date: "2026-09-30"
      record: "Panel photo shows '21.5 °C' after entering 21.5C and '21.1 °C' after 70F."

6. The build¶

The BUILD.bazel file wires it together — the model with its lock, one test per hook, an annotation check, and the evidence → report → golden chain, with the lock checked against the same evidence:

rr_py_test(
    name = "controller_test",
    srcs = ["tests/test_controller.py"],
    deps = [
        ":thermostat",
        requirement("pytest"),
    ],
)

py_test(
    name = "display_test",
    srcs = ["tests/display_test.py"],
    deps = [
        ":thermostat",
        "@rules_requirements//python",
    ],
)

cc_test(
    name = "interlock_test",
    srcs = ["interlock/interlock_test.cc"],
    deps = [
        ":interlock",
        "@googletest//:gtest_main",
        "@rules_requirements//cc:gtest",
    ],
)

rr_rust_test(
    name = "setpoint_test",
    crate = ":setpoint",
    rule = rust_test,
    deps = ["@rules_requirements//rust:rr"],
)

SOURCES = glob([
    "thermostat/*.py",
    "interlock/*",
    "setpoint/src/*.rs",
    "tests/*.py",
])

# Every @rr(...) annotation must name an entity that exists.
rr_annotations_test(
    name = "annotations_test",
    srcs = SOURCES,
    model = ":model",
)

# --------------------------------------------------------------------------- #
# Evidence and the traceability report, pinned by goldens.                     #
# --------------------------------------------------------------------------- #

rr_evidence(
    name = "evidence",
    tests = [
        ":controller_test",
        ":display_test",
        ":interlock_test",
        ":setpoint_test",
    ],
)

EVIDENCE = [
    ":evidence",
    "evidence/panel_inspection.rr.yaml",
]

# A quarantined test case (one naming two requirements, or claimed by two)
# fails this build; :report_check_test re-proves from report.json alone that
# no test case verifies two requirements.
rr_report(
    name = "report",
    srcs = SOURCES,
    check = True,
    evidence = EVIDENCE,
    model = [":model"],
)

# The lock agrees with the evidence: no member missing, none unlocked, no
# owner changed (`rr sets check`). `bazel run //:sets_lock_test.update`
# rewrites requirements/verification.rrlock after an intended change.
rr_sets_lock_test(
    name = "sets_lock_test",
    evidence = EVIDENCE,
    model = ":model",
)

rr_golden_test(
    name = "report_json_golden_test",
    src = ":report.json",
    golden = "report.golden.json",
)

rr_golden_test(
    name = "report_md_golden_test",
    src = ":report.md",
    golden = "report.golden.md",
)

# `bazel run //:editor` — the web editor on this model (see the web editor guide).
rr_editor(
    name = "editor",
    model = ":model",
    paths = ["requirements"],
)

$ bazel test //...
//:annotations_test                                                      PASSED
//:controller_test                                                       PASSED
//:display_test                                                          PASSED
//:interlock_test                                                        PASSED
//:model_test                                                            PASSED
//:report_check_test                                                     PASSED
//:report_json_golden_test                                               PASSED
//:report_md_golden_test                                                 PASSED
//:setpoint_test                                                         PASSED
//:sets_lock_test                                                        PASSED
$ bazel build //:report
evidence: 5 file(s), 18 test case(s) | validation: 2/2 needs | verification: 7/7 requirements (0 failed, 0 unverified, 0 under-verified, 0 invalid, 0 incomplete) | risks: 2/2 mitigated | gaps: 0

//:report runs the four test targets inside a build action (rr_evidence), adds the inspection record, scans the sources for annotations and renders bazel-bin/report.html, report.json and report.md. A quarantined test case would fail this build. //:report_check_test re-proves from report.json alone that no test case is owned by two requirements (rr check-report).

The lock. requirements/verification.rrlock records, for every test case, the one requirement whose set holds it:

# Generated by `rr sets lock --write`; review its diff like a golden file.
schema: rules_requirements/verification-lock/v1
cases:
  //:controller_test:
    "tests.test_controller::test_accepts_range_limits": REQ-4
    "tests.test_controller::test_heats_below_band": REQ-1
    "tests.test_controller::test_invalid_reading_turns_heater_off[85.1]": REQ-6
    "tests.test_controller::test_invalid_reading_turns_heater_off[-41.0]": REQ-6

//:sets_lock_test fails when the evidence and the lock disagree — a locked test that no longer runs, a new test no one locked, a case that changed owner — so a deleted or renamed test cannot silently shrink a requirement’s set. After an intended change, bazel run //:sets_lock_test.update rewrites the lock; its diff is reviewed with the change, like a golden file.

7. The report¶

This is the example’s golden Markdown report, exactly as checked in. Every requirement is verified, by a set of test cases it alone owns: each member lists the selector that claims it (via model), and the “Case attribution” table shows every case of every target owned once, none unowned, none quarantined:

Thermostat¶

2/2 user needs validated · 7/7 requirements verified (0 under-verified, 0 failed, 0 invalid, 0 incomplete, 0 unverified) · 2/2 risks mitigated · 18 test cases (18 owned, 0 unowned, 0 quarantined) · 0 gaps

attribution: model · lock: requirements/verification.rrlock

User needs — validation¶

ID	Need	Requirements	Status
UN-1	Keep the room at a comfortable temperature	REQ-1, REQ-2	✅ VALIDATED
UN-2	Set the target temperature in Celsius or Fahrenheit	REQ-3, REQ-4, REQ-7	✅ VALIDATED

Requirements — verification¶

ID	Requirement	Traces	Demands	Evidence	Status
REQ-1	Heat when the room is below the setpoint band	satisfies UN-1	simulation	set 1/1 passed ✓ tests.test_controller::test_heats_below_band [simulation]	✅ VERIFIED
REQ-2	Stop heating above the band; hold state inside it	satisfies UN-1	simulation	set 1/1 passed ✓ tests.test_controller::test_stops_above_band_and_holds_inside_it [simulation]	✅ VERIFIED
REQ-3	Parse setpoints in °C and °F	satisfies UN-2; implements MIT-2	simulation	set 2/2 passed ✓ tests::parses_celsius_and_fahrenheit [simulation] ✓ tests::requires_a_unit [simulation]	✅ VERIFIED
REQ-4	Reject setpoints outside 5-30 °C	satisfies UN-2; implements MIT-2	simulation	set 6/6 passed ✓ tests.test_controller::test_accepts_range_limits [simulation] ✓ tests.test_controller::test_rejects_setpoints_outside_range[30.1] [simulation] ✓ tests.test_controller::test_rejects_setpoints_outside_range[4.9] [simulation] ✓ tests.test_controller::test_rejects_setpoints_outside_range[80.0] [simulation] ✓ tests::checks_the_range_after_converting [simulation] ✓ tests::rejects_out_of_range [simulation]	✅ VERIFIED
REQ-5	Independent over-temperature cutoff	implements MIT-1	sil	set 3/3 passed ✓ Interlock::NanReadingTrips [sil] ✓ Interlock::StaysTrippedUntilBelowReset [sil] ✓ Interlock::TripsAtLimit [sil]	✅ VERIFIED
REQ-6	Fail safe on an invalid sensor reading	implements MIT-1	simulation	set 3/3 passed ✓ tests.test_controller::test_invalid_reading_turns_heater_off[-41.0] [simulation] ✓ tests.test_controller::test_invalid_reading_turns_heater_off[85.1] [simulation] ✓ tests.test_controller::test_invalid_reading_turns_heater_off[nan] [simulation]	✅ VERIFIED
REQ-7	Show the setpoint with its unit	satisfies UN-2	inspection	set 2/2 passed ✓ display_test.DisplayTest::test_setpoint_shows_unit [simulation] ✓ inspection.TM-2::panel-shows-setpoint-unit [inspection]	✅ VERIFIED

Risks — control¶

ID	Risk	Severity × likelihood	Mitigations	Status
RISK-1	Room overheats	high × possible → high × rare	MIT-1	✅ MITIGATED
RISK-2	Implausible setpoint accepted	medium × likely → medium × unlikely	MIT-2	✅ MITIGATED

Mitigations — risk control measures¶

ID	Mitigation	Type	Mitigates	Implemented by	Status
MIT-1	Independent over-temperature protection	protective	RISK-1	REQ-5, REQ-6	✅ VERIFIED
MIT-2	Validate setpoints at entry	inherent	RISK-2	REQ-3, REQ-4	✅ VERIFIED

Test methods¶

ID	Method	Level	Used by
TM-1	Interlock software-in-the-loop test	sil	REQ-5
TM-2	Visual inspection of the panel	inspection	REQ-7

Implementation — source annotations¶

ID	Implemented in	Verified in
REQ-1	thermostat/controller.py:27 (class Controller)	tests/test_controller.py:9 (def test_heats_below_band)
REQ-2	thermostat/controller.py:27 (class Controller)	tests/test_controller.py:15 (def test_stops_above_band_and_holds_inside_it)
REQ-3	setpoint/src/lib.rs:24 (fn parse)	setpoint/src/lib.rs:46 (fn parses_celsius_and_fahrenheit) setpoint/src/lib.rs:54 (fn requires_a_unit)
REQ-4	setpoint/src/lib.rs:24 (fn parse) thermostat/controller.py:20 (def check_setpoint)	setpoint/src/lib.rs:62 (fn rejects_out_of_range) setpoint/src/lib.rs:72 (fn checks_the_range_after_converting) tests/test_controller.py:24 (def test_rejects_setpoints_outside_range) tests/test_controller.py:31 (def test_accepts_range_limits)
REQ-5	interlock/interlock.h:7 (class Interlock)	interlock/interlock_test.cc:13 (Interlock.TripsAtLimit) interlock/interlock_test.cc:22 (Interlock.StaysTrippedUntilBelowReset) interlock/interlock_test.cc:33 (Interlock.NanReadingTrips)
REQ-6	thermostat/controller.py:14 (def plausible)	tests/test_controller.py:37 (def test_invalid_reading_turns_heater_off)
REQ-7	thermostat/display.py:5 (def format_setpoint)	tests/display_test.py:11 (def test_setpoint_shows_unit)
MIT-1	—	—
MIT-2	—	—

Modules¶

Module	Status
interlock	✅ VERIFIED
setpoint	✅ VERIFIED
thermostat	✅ VERIFIED

Verification sets¶

Each entity’s set: the cases it owns, the cases it expects (literal selectors, the lock) and every quarantined case that names it. It is verified only when the whole set passed together.

REQ-1 — ✅ VERIFIED¶

set 1/1 passed

Case	State	Level	Via	Selector	Note
//:controller_test#tests.test_controller::test_heats_below_band	passed	simulation	model	tests.test_controller::test_heats_below_band

REQ-2 — ✅ VERIFIED¶

set 1/1 passed

Case	State	Level	Via	Selector	Note
//:controller_test#tests.test_controller::test_stops_above_band_and_holds_inside_it	passed	simulation	model	tests.test_controller::test_stops_above_band_and_holds_inside_it

REQ-3 — ✅ VERIFIED¶

set 2/2 passed

Case	State	Level	Via	Selector	Note
//:setpoint_test#tests::parses_celsius_and_fahrenheit	passed	simulation	model	tests::parses_celsius_and_fahrenheit
//:setpoint_test#tests::requires_a_unit	passed	simulation	model	tests::requires_a_unit

REQ-4 — ✅ VERIFIED¶

set 6/6 passed

Case	State	Level	Via	Selector
//:controller_test#tests.test_controller::test_accepts_range_limits	passed	simulation	model	tests.test_controller::test_accepts_range_limits
//:controller_test#tests.test_controller::test_rejects_setpoints_outside_range[4.9]	passed	simulation	model	tests.test_controller::test_rejects_setpoints_outside_range[*]
//:controller_test#tests.test_controller::test_rejects_setpoints_outside_range[30.1]	passed	simulation	model	tests.test_controller::test_rejects_setpoints_outside_range[*]
//:controller_test#tests.test_controller::test_rejects_setpoints_outside_range[80.0]	passed	simulation	model	tests.test_controller::test_rejects_setpoints_outside_range[*]
//:setpoint_test#tests::checks_the_range_after_converting	passed	simulation	model	tests::checks_the_range_after_converting
//:setpoint_test#tests::rejects_out_of_range	passed	simulation	model	tests::rejects_out_of_range

REQ-5 — ✅ VERIFIED¶

set 3/3 passed

Case	State	Level	Via	Selector
//:interlock_test#Interlock::NanReadingTrips	passed	sil	model	Interlock::*
//:interlock_test#Interlock::StaysTrippedUntilBelowReset	passed	sil	model	Interlock::*
//:interlock_test#Interlock::TripsAtLimit	passed	sil	model	Interlock::*

REQ-6 — ✅ VERIFIED¶

set 3/3 passed

Case	State	Level	Via	Selector
//:controller_test#tests.test_controller::test_invalid_reading_turns_heater_off[85.1]	passed	simulation	model	tests.test_controller::test_invalid_reading_turns_heater_off[*]
//:controller_test#tests.test_controller::test_invalid_reading_turns_heater_off[-41.0]	passed	simulation	model	tests.test_controller::test_invalid_reading_turns_heater_off[*]
//:controller_test#tests.test_controller::test_invalid_reading_turns_heater_off[nan]	passed	simulation	model	tests.test_controller::test_invalid_reading_turns_heater_off[*]

REQ-7 — ✅ VERIFIED¶

set 2/2 passed

Case	State	Level	Via	Selector	Note
//:display_test#display_test.DisplayTest::test_setpoint_shows_unit	passed	simulation	model	display_test.DisplayTest::test_setpoint_shows_unit
record:panel_inspection#inspection.TM-2::panel-shows-setpoint-unit	passed	inspection	model	inspection.TM-2::panel-shows-setpoint-unit

Case attribution¶

Target	Cases	Owned	Owners
//:controller_test	9	9	REQ-1, REQ-2, REQ-4, REQ-6
//:display_test	1	1	REQ-7
//:interlock_test	3	3	REQ-5
//:setpoint_test	4	4	REQ-3, REQ-4
record:panel_inspection	1	1	REQ-7

8. Things to try¶

Change something and watch the golden test tell you what it did to the traceability argument:

Demand more rigor. Point REQ-5’s method at a new test method with level: hil. REQ-5 becomes UNDER-VERIFIED (its evidence is sil), MIT-1 and RISK-1 become PARTIAL, and RISK-1 — a high-severity risk — is hoisted into the “not mitigated” banner. The gap queue gains an under-verified item routed to human-gate, a high-risk-open item, and a pyramid item.
Break the code. Remove the hysteresis in thermostat/controller.py: REQ-2 turns FAILED, and with it UN-1’s validation and the golden test.
Lose the sign-off. Delete evidence/panel_inspection.rr.yaml from the report’s evidence: REQ-7’s claimed inspection record did not run, so its set is not whole — REQ-7 reads INCOMPLETE and UN-2 PARTIAL — and the incomplete gap is routed to human-gate, because the missing member is an inspection (the claim’s level).
Name two requirements in one test. Put rr::verifies!("REQ-3", "REQ-4") back into requires_a_unit: the case is quarantined, REQ-3 and REQ-4 read INVALID, and bazel build //:report fails (rr report exits 3) with an ATTRIBUTION ERROR: multi-tag line naming the case.
Claim one case twice. Add tests::requires_* to REQ-4’s claims on //:setpoint_test: //:model_test fails with the shared-case error shown in step 3, before any test runs.

Accept an intended change with bazel run //:report_md_golden_test.update (and its json twin); the diff of the golden file is the change to the traceability argument, reviewed alongside the code.