The frontmatter lists a proof scenario or finding for every required rule and records each applicable category. Scenario coverage describes what to check; bindings identify the assertions that already exist, and execution results remain unverified. The maximum-size scenario is unbound, and denial of register read access lacks a dedicated existing assertion. Workflow edges not named by a scenario remain in this finding rather than gaining a binding from shared workflow membership.
Kind selection governs creation and domain ownership. The register contains active Accounting and Membership kinds and an inactive Events kind. Read the kinds, create suitable products through their owning callers, and try the inactive and cross-owner choices. Successful records match the selected kind; inactive and cross-owner choices leave no new product.
Coverage
Rulecovered
Transitionnot-applicable
Validationgap: FND-ACC-PRD-071
Permissioncovered
Edgegap: FND-ACC-PRD-071
Failuregap: FND-ACC-PRD-071
Boundarycovered
Concurrencynot-applicable
Invariantcovered
Interactioncovered
Test Scenarios
6 scenarios proving CAP-ACC-PRD-001; 4 bound to an existing test.
01Release control protects product kindsinvariantunitnegativetest