Rite: Authorization Proof

Authorization bugs often hide outside the path ordinary tests exercise. A customer endpoint may enforce ownership while a support endpoint reaches the same sensitive effect without the same check. Reviewers can inspect one function, see a guard, and still miss the bypass. Rite makes that review workflow explicit. A developer writes the authorization rule, names the entry paths and sensitive sink, and provides a small adapter that exposes observable effects. Rite runs the same literal cases through every mapped entry and records whether the expected result, sink calls, events, and state changes match. It does not treat a crash or an unexecuted branch as security evidence. The included refund sample demonstrates the complete loop. The vulnerable baseline records an unauthorized refund through `supportRefund`. Both entry paths are then routed through a shared authorization gate and all ten mapped checks pass. Rite removes the ownership guard once, confirms both wrong-owner cases fail with the forbidden effect, restores the exact fixed source, and passes again. This bounded mutation shows that the checks detect the defect they claim to cover. IBM Bob IDE was used as the development workflow for defining the policy and cases, tracing both paths, applying the shared repair, and structuring the four-phase proof. The repository preserves that process as a reusable Bob skill at `.bob/skills/rite/SKILL.md`. Rite also exposes the same verifier through a CLI and an MCP server, while the read-only GitHub App reads workflow artifacts and rejects a report whose commit SHA does not match the selected run. Rite is a working prototype with deliberately bounded claims. The public demo uses synthetic in-memory data and checks two named paths. It does not infer that unmapped paths are safe, does not move money, and does not claim exhaustive analysis of arbitrary repositories.