Files
openzeppelin-contracts/certora/scripts/passes/verifyGPLQ_proposalInOneState.sh
teryanarmen e04f7ded94 Fixed GPLQ spec, all rules passing (#3822)
Co-authored-by: Michael George <michael@certora.com>
Co-authored-by: Nick Armstrong <nick@certora.com>
Co-authored-by: Michael George <mdgeorge@cs.cornell.edu>
Co-authored-by: Aleksander Kryukov <firealexkryukov@gmail.com>
Co-authored-by: Hadrien Croubois <hadrien.croubois@gmail.com>
2022-11-27 20:41:50 -03:00

14 lines
436 B
Bash

#!/usr/bin/env bash
set -euxo pipefail
certoraRun \
certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorFullHarness.sol certora/munged/governance/TimelockController.sol \
--verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \
--link GovernorFullHarness:token=ERC20VotesHarness \
--optimistic_loop \
--rule proposalInOneState \
--settings -t=1000 \
--loop_iter 1 \
$@