Skip to content

IDE Formal Evidence Execution Plan

Status: Internal freeze execution plan Owner: BionicLoop engineering Last updated: 2026-04-07 12:32 EDT

Purpose

Define the formal evidence execution set for the current IDE software packet.

This plan is scoped to the claims in the current packet.

Current Starting Point

The current packet is ready for review, but formal evidence promotion is still pending:

  • the formal evidence lane at /Users/jcostik/BionicLoop/Docs/Quality/Evidence/Formal/ is not yet populated with promoted freeze artifacts for the claimed software baseline
  • the RTM audit currently stands at:
  • 0 formal-ready
  • 15 rerun-needed
  • 1 deferred partial-scope row (RA-009)

Lean Freeze Principle

For the current IDE packet, formal evidence execution should be limited to protocol lanes that are necessary to support the accepted local software baseline:

  • run what is required to support claimed local software behavior
  • defer what remains intentionally out of scope
  • avoid adding new verification scope during freeze execution

Minimum Protocol Set

1. Required for the current packet

Protocol Why It Must Run Primary Coverage
STP-ALG-001.md Algorithm-host and bridge behavior are core to the investigational controller claim. RA-014, TV-ALG-001..011
STP-AUTO-001.md Most accepted local software behavior is automated and should be closed here. RA-001, RA-002, RA-003, RA-004, RA-005, RA-006, RA-008, RA-010, RA-011, RA-012, RA-013, RA-016, plus local RA-009 / TV-SEC-001

2. Run only if these behaviors remain explicitly claimed at freeze

Protocol When It Is Required Primary Coverage
STP-HW-001.md If freeze-time package still claims live reconnect, live interruption timing, pod-card live transitions, delivery-state clear on live refresh, and other true hardware-only behaviors. RA-007, hardware portions of RA-015, selected live portions of meal/pump/state rows
STP-ALERT-001.md If freeze-time package still claims operator-observed alert wording, background-notification behavior, and manual/system interruption-alert behavior beyond automated subsets. Manual/system portions of RA-011, selected alert parts of RA-015

Phase 1. Freeze candidate lock

  1. choose the freeze candidate SHA
  2. fill the SHA placeholder in controlled docs at freeze time
  3. confirm the packet scope/defer list is unchanged

Phase 2. Required formal execution

  1. execute STP-ALG-001
  2. execute STP-AUTO-001
  3. execute TV-SEC-001 within the STP-AUTO-001 run using Cybersecurity_TV_SEC_001_Freeze_Execution_Checklist.md

Phase 3. Conditional formal execution

  1. run STP-HW-001 only for hardware behaviors still explicitly claimed
  2. run STP-ALERT-001 only for manual/system alert behaviors still explicitly claimed

Phase 4. Trace promotion

  1. replace working-lane evidence references for claimed rows with formal STR references
  2. leave deferred rows explicitly deferred rather than half-closed
  3. update RTM status for each claimed row from In progress to either:
  4. Complete, or
  5. Deferred (partial scope) / deferred equivalent with rationale

STP-ALG-001

Use this protocol to close:

  • all claimed TV-ALG-* rows
  • the algorithm-specific RTM row RA-014

STP-AUTO-001

Use this protocol to close the automated/local-software surface in the current packet:

  • runtime policy rows
  • CGM policy rows
  • automated pump policy rows
  • meal/BG/local-state rows
  • clinical settings rows
  • UI rows
  • automated alert rows
  • local telemetry/logging rows that remain in scope
  • TV-SEC-001

STP-HW-001 and STP-ALERT-001

Treat these as claim-driven, not automatic.

If the receiving team decides the current freeze package can rely on automated evidence plus explicit defer for remaining live/manual portions, do not widen the freeze set unnecessarily.

Output Artifacts Expected

At minimum, the freeze package should produce:

  • formal STR-ALG-001 bundle
  • formal automated STR bundle(s) for STP-AUTO-001
  • formal STR-SEC-001 evidence for TV-SEC-001
  • optional formal STR-HW-001 and STR-ALERT-001 only if those live/manual claims remain in scope

Prepared shell paths now exist for the current freeze set:

Prepared execution runbook now exists at:

Decision Rule For The Receiving Team

Before scheduling hardware/manual reruns, first answer:

  • is this behavior still explicitly claimed in the current packet?

If the answer is no, defer it explicitly. If the answer is yes, run the owning protocol and promote formal evidence.

Primary Support References