DesignProof: Code That Does What Your Policy Says

66% of developers say AI generated code is "almost right, but not quite" (Stack Overflow Developer Survey 2025). The most dangerous "not quite" hides in permission logic: who can access what. These bugs pass unit tests and code review, because tests only check the cases someone thought of, and they end up as data leaks. DesignProof improves the code review workflow for permission logic. IBM Bob 2.0 reads a plain English policy document and the application code, using parallel subagents: one extracts the rules, one traces how the code enforces them. Bob then writes an Alloy 6 model of what the code actually does, with one assertion per policy rule. Our designproof.py checker runs the Alloy Analyzer, which searches every combination of users, teams, files, and share links up to scope 4 for a counterexample. For each violation, Bob writes a failing test, applies a minimal fix, and rechecks until every rule is verified. We demonstrated it on a sample FastAPI file sharing app whose 4 existing tests all passed. DesignProof found that a user removed from a team could still edit the team's files through an old share link. The first fix then introduced a second bug, which was not planted: re-added members were wrongly blocked. Bob found it, and Alloy confirmed it by rechecking the model of the code after fix 1. After both fixes, all rules are verified and tests grew from 4 to 20. The workflow is packaged as a reusable DesignProof custom mode in IBM Bob, a command line checker, and a GitHub Actions workflow that fails the build whenever a modeled rule is violated. A live Streamlit dashboard runs Alloy on the server so anyone can reproduce the results. IBM Bob features used: Plan mode, parallel subagents, document understanding, Agent mode, and a custom mode. Honest limits: Alloy checks are complete up to the chosen scope, and every finding is confirmed by a real failing test against the actual code.