B-4 · Medium

planarian @ a924e09 · Spec v4.6 · snapshot main · all versions

decide is proved, but its inputs (DerivedFacts, Authorization) are computed by unproven code

Breaks	Status	Mitigation	Closes in
Correct (inputs)	Open (v4.5 §17a)	Internal-unproven count reported separately; fail-closed defaults; `derive` proved in C	A accounting; C proof

The guarantees it narrows