Proof · Engineering practice
How do I connect hazard analysis to code and verified fixes?
Connect a hazard to the behavior that could cause harm, the requirement that controls it, the implementing change and the evidence that tests the mitigation. Record the remaining risk and who may accept it. Considering a catalog entry is the start of that chain, not proof that the risk is controlled.
A shared WebSocket introduces several distinct risks
This example is adapted from Proof’s hazard-analysis help. One requirement shares a WebSocket across browser tabs. The review considers concurrency, atomicity and slow consumers, then records why each candidate applies or does not.
| Candidate | Disposition | Next obligation |
|---|---|---|
| concurrent_invariant_preserved | Accept: tabs share mutable connection state. | Specify the invariant and exercise relevant interleavings. |
| compound_operation_atomic | Accept: connect-and-subscribe can partially fail. | Check failure between connection and subscription, including cleanup. |
| redos_resistant | Suppress only if no relevant untrusted-string processing exists. | Retain that concrete scope rationale and reassess if parsing changes. |
| cache_version_coherent | Suppress if no cached projection exists. | Keep the architectural assumption visible. |
| shared_connection_back_pressure_bounded | Draft a project-specific class. | Define queue bounds and the outcome for a slow tab. |
An accepted obligation still needs mitigation and evidence. A suppression is a scoped non-applicability decision; a required but unfinished mitigation must remain open or explicitly deferred.
Carry the slow-tab risk through to an observation
Illustrative extension: one stalled tab must not exhaust shared memory or stop delivery to healthy tabs. Record the exposure condition, consequence, owner and the policy for dropping, disconnecting or buffering a slow consumer.
| Step | Record to keep |
|---|---|
| Mitigation requirement | Bound each tab’s queue; preserve delivery to healthy tabs under the declared load. |
| Implementation | Link the queue limit, overflow decision and disconnect path to the requirement. |
| Execution | Drive one consumer slowly and another normally; record queue size, memory, delivery and recovery outcomes. |
| Residual risk | State the untested load range and the effect of disconnecting a slow consumer. |
| Closure decision | Accept only the scope supported by those observations, under the applicable authority. |
This is an evidence plan, not an executed benchmark. The run must identify its revision, load, duration and environment before anyone claims the mitigation works. A finite stress test also does not establish every scheduling or exhaustion condition.
Use catalog checks to maintain the review record
proof catalog list
proof catalog show concurrent_invariant_preserved
proof audit --check obligation_baseline
proof audit --check code_signal_obligations_reviewed
proof audit --check obligation_evidence_complete --verbose
The baseline check identifies unresolved catalog obligations in its scope. Code signals can suggest relevant classes for review. The evidence check examines required class/evidence relationships and applicable provenance. None of these checks alone executes the slow-consumer experiment or establishes residual-risk acceptability.
proof catalog new shared_connection_back_pressure_bounded --category domain --domain concurrency
proof req edit SYS-REQ-001 --add-obligation shared_connection_back_pressure_bounded
These authoring examples create and attach a project class. Its definition, assumptions and required evidence still need review. Retain the catalog version and decision rationale so a later change can identify what needs reassessment.
Distinguish a fixed witness from a closed failure class
A reproduced slow-tab failure that passes after the patch establishes repair of that instance. Permanent regression protection preserves the lesson. Broader class closure needs the declared obligations for related interleavings, disconnects and load conditions; unchecked siblings remain open.
Hazard analysis may use methods such as FMEA or STPA alongside the software catalog. The catalog is not an exhaustive hazard-identification method or a replacement for a project safety assessment. Keep requirements, mitigation evidence and authorized residual-risk decisions connected so later agents can retrieve the obligation instead of reconstructing it.
See checking every declared evidence obligation and showing remaining gaps in the report.