This repository demonstrates ReqProof on a Solidity governance system modeled after the Beanstalk-style same-block governance drain. It uses an OpenZeppelin-style Governor + TimelockController composition, Foundry tests, Solidity code-signal obligations, Slither signal import, and Z3-backed requirements.
The primary writeups are:
- Proposal activation is delayed by the configured voting delay.
- Vote weight is read from the proposal snapshot, not current balances.
- Timelock execution requires
scheduled_at + min_delay. - Timelock predecessor, role-gate, cancellation, duplicate-operation, operation-identity, voting-delay, and voting-period invariants are formalized and checked.
- Treasury zero-owner, zero-recipient, owner-only mutation, full-balance drain, failed-call atomicity, and reentrancy-guard behavior are tested.
- Token mint authority, delegated voting power, and immutable past-vote snapshots are tested.
- The unsafe same-block execution path is represented by
UnsafeGovernor; the fixed path routes execution throughMyTimelock.
Clone with submodules so the pinned OpenZeppelin dependency and its Foundry test dependency are present:
git clone --recurse-submodules https://github.com/probelabs/proof-solidity-demo.gitforge build
forge test
proof audit --fail-level warnThe audit is configured to refresh Slither-derived signals, but the Slither
target is intentionally narrowed to src and excludes vendored/build/cache
paths. For large Solidity projects, run heavyweight analyzers inside a
container or CI job with a hard memory limit and import their JSON/SARIF output
instead of running them directly during local audit.