Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Certora Run Github Application #32

Open
wants to merge 5 commits into
base: main
Choose a base branch
from
Open

Certora Run Github Application #32

wants to merge 5 commits into from

Conversation

H00N24
Copy link
Collaborator

@H00N24 H00N24 commented Jan 9, 2025

In this PR we're adding support for the new Certora Run GitHub Application (https://github.com/Certora/certora-run-action)

@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 9, 2025

Certora Run Started (AAVE Governance V3 Execution Chain)

  • Group ID: 5ef47c91-7763-42bd-9182-ab2af55e0552
Config Status Link Log File
action_access_level_isnt_null_after_createPayload Submited link security/certora/confs/payloads/verifyPayloadsController.conf-78b775683406.log
action_callData_immutable Submited link security/certora/confs/payloads/verifyPayloadsController.conf-0a12748633ac.log
action_immutable_check_only_fixed_size_fields Submited link security/certora/confs/payloads/verifyPayloadsController.conf-c42ed512db47.log
action_signature_immutable Submited link security/certora/confs/payloads/verifyPayloadsController.conf-ae6ea9c222ff.log
checkUpdateExecutors checkUpdateExecutors_witness_1 checkUpdateExecutors_witness_2 checkUpdateExecutors_witness_3 checkUpdateExecutors_witness_4 Submited link security/certora/confs/payloads/verifyPayloadsController.conf-62b427dbd9e1.log
delay_of_executor_of_max_access_level_within_range Submited link security/certora/confs/payloads/verifyPayloadsController.conf-42f682b12756.log
executedAt_is_zero_before_executed Submited link security/certora/confs/payloads/verifyPayloadsController.conf-899a86cc2637.log
executed_after_queue_state_variable zero_executedAt_if_not_executed_state_variable Submited link security/certora/confs/payloads/verifyPayloadsController.conf-4dfaa43785e9.log
executed_when_in_queued_state executed_when_in_queued_state_variable guardian_can_cancel no_late_cancel state_variable_cant_decrease Submited link security/certora/confs/payloads/verifyPayloadsController.conf-666f10dd9046.log
executor_exists_after_createPayload Submited link security/certora/confs/payloads/verifyPayloadsController.conf-e503864ede12.log
executor_exists_if_action_not_null Submited link security/certora/confs/payloads/verifyPayloadsController.conf-27c2640ec287.log
executor_exists_iff_action_not_null Submited link security/certora/confs/payloads/verifyPayloadsController.conf-d9356d60a972.log
executor_exists_only_if_action_not_null Submited link security/certora/confs/payloads/verifyPayloadsController.conf-ede295228643.log
executor_isnt_used_twice executor_of_level_null_is_zero Submited link security/certora/confs/payloads/verifyPayloadsController.conf-1332c1361a5b.log
executor_of_maximumAccessLevelRequired_exists Submited link security/certora/confs/payloads/verifyPayloadsController.conf-8ae73a6ea388.log
executor_of_maximumAccessLevelRequired_exists_after_createPayload Submited link security/certora/confs/payloads/verifyPayloadsController.conf-1b0a16d507fd.log
nonempty_actions Submited link security/certora/confs/payloads/verifyPayloadsController.conf-02d981bf7fb8.log
null_access_level_iff_state_is_none Submited link security/certora/confs/payloads/verifyPayloadsController.conf-68bac8ee4b2d.log
payload_delay_within_range Submited link security/certora/confs/payloads/verifyPayloadsController.conf-45f64d070070.log
payload_maximal_access_level_gt_action_access_level state_cant_decrease no_transition_beyond_state_gt_3 no_transition_beyond_state_variable_gt_3 no_queue_after_expiration empty_actions_if_out_of_bound_payload expirationTime_equal_to_createAt_plus_EXPIRATION_DELAY empty_actions_iff_uninitialized null_access_level_if_out_of_bound_payload null_creator_and_zero_expiration_time_if_out_of_bound_payload empty_actions_only_if_uninitialized_payload executor_access_level_within_range consecutiveIDs empty_actions_if_uninitialized_payload queued_before_expiration_delay payload_grace_period_eq_global_grace_period null_access_level_only_if_out_of_bound_payload null_state_variable_if_out_of_bound_payload created_in_the_past queued_after_created executed_after_queue queuedAt_is_zero_before_queued no_early_cancellation execute_before_delay__maximumAccessLevelRequired action_immutable_fixed_size_fields initialized_payload_fields_are_immutable payload_fields_immutable_after_createPayload method_reachability Submited link security/certora/confs/payloads/verifyPayloadsController.conf-8a31301fe2d3.log
payload_state_transition_post_state payload_state_transition_pre_state Submited link security/certora/confs/payloads/verifyPayloadsController.conf-6e013c7cd1fc.log
queuedAt_is_zero_before_queued_state_variable executedAt_is_zero_before_executed_state_variable null_state_equivalence Submited link security/certora/confs/payloads/verifyPayloadsController.conf-20abbecf70a7.log
zero_executedAt_if_not_executed Submited link security/certora/confs/payloads/verifyPayloadsController.conf-9483ac6e1ba1.log

Certora Run Summary

  • Started 23 jobs
  • 0 jobs failed

Download Logs

@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 9, 2025

Certora Run Started (AAVE Governance V3 Mainnet)

  • Group ID: 46c29fa8-1dfa-4370-9ea8-ba3162040930
Config Status Link Log File
Governance.conf --rule at_least_single_payload_active empty_payloads_iff_uninitialized_proposal Submited link security/certora/confs/verifyGovernance.conf-5b7efc0e1118.log
Governance.conf --rule cancellationFeeZeroForFutureProposals null_state_variable_iff_null_access_level zero_voting_portal_iff_uninitialized_proposal Submited link security/certora/confs/verifyGovernance.conf-f97a2ef22a3c.log
Governance.conf --rule cannot_queue_when_voting_portal_unapproved only_owner_can_set_voting_config_witness only_owner_can_set_voting_config single_state_transition_per_block_non_creator_witness Submited link security/certora/confs/verifyGovernance.conf-6995ba55d594.log
Governance.conf --rule check_new_representative_set_size_after_updateRepresentatives check_old_representative_set_size_after_updateRepresentatives Submited link security/certora/confs/verifyGovernance.conf-5ff62d0c2ed6.log
Governance.conf --rule check_new_representative_set_size_after_updateRepresentatives_witness_antecedent_first check_new_representative_set_size_after_updateRepresentatives_witness_antecedent_second check_new_representative_set_size_after_updateRepresentatives_witness_consequent_first check_new_representative_set_size_after_updateRepresentatives_witness_consequent_second Submited link security/certora/confs/verifyGovernance.conf-1305435cb87f.log
Governance.conf --rule creator_is_not_zero creator_of_initialized_proposal_is_not_zero null_state_equivalence Submited link security/certora/confs/verifyGovernance.conf-bc28d4006c4b.log
Governance.conf --rule immutable_after_creation_witness_access_level immutable_after_creation_witness_creation_time immutable_after_creation_witness_ipfs_hash Submited link security/certora/confs/verifyGovernance.conf-471c65df4d74.log
Governance.conf --rule immutable_after_creation_witness_creator immutable_after_creation_witness_voting_portal Submited link security/certora/confs/verifyGovernance.conf-1a6192e27db9.log
Governance.conf --rule immutable_after_creation_witness_payload_length immutable_after_activation_witness only_state_changing_function_initiate_transitions__pre_state Submited link security/certora/confs/verifyGovernance.conf-dbe6e3134d1e.log
Governance.conf --rule insufficient_proposition_power_witness_time_elapsed Submited link security/certora/confs/verifyGovernance.conf-cf9ae3e98e32.log
Governance.conf --rule no_representative_is_zero_2 no_representative_of_zero Submited link security/certora/confs/verifyGovernance.conf-d72a6f46b143.log
Governance.conf --rule no_self_representative no_representative_is_zero consecutiveIDs totalCancellationFeeEqualETHBalance zero_address_is_not_a_valid_voting_portal Submited link security/certora/confs/verifyGovernance.conf-494713c96172.log
Governance.conf --rule null_state_iff_uninitialized_proposal setInvariant addressSetInvariant Submited link security/certora/confs/verifyGovernance.conf-3e6bd6c7ab3a.log
Governance.conf --rule only_state_changing_function_initiate_transitions__post_state Submited link security/certora/confs/verifyGovernance.conf-c41645206578.log
Governance.conf --rule only_valid_voting_portal_can_queue_proposal immutable_after_activation immutable_after_creation only_guardian_can_cancel guardian_can_cancel Submited link security/certora/confs/verifyGovernance.conf-5e6e6229cc4e.log
Governance.conf --rule proposal_after_voting_portal_invalidate insufficient_proposition_power insufficient_proposition_power_witness_state_is_failed insufficient_proposition_power_witness_state_is_cancelled insufficient_proposition_power_witness_time_elapsed Submited link security/certora/confs/verifyGovernance.conf-e670dd00afba.log
Governance.conf --rule proposal_voting_duration_lt_expiration_time config_voting_duration_lt_expiration_time proposal_state_transition_post_state proposal_state_transition_pre_state Submited link security/certora/confs/verifyGovernance.conf-50d3aa08ef83.log
Governance.conf --rule single_state_transition_per_block_non_creator_non_guardian state_cant_decrease no_state_transitions_beyond_3 immutable_voting_portal Submited link security/certora/confs/verifyGovernance.conf-38bc78a8ce8a.log
Governance.conf --rule state_changing_function_cannot_be_called_while_in_terminal_state proposal_executes_after_cooldown_period Submited link security/certora/confs/verifyGovernance.conf-a8f9b0669c8c.log
Governance.conf --rule state_changing_function_self_check state_variable_changing_function_self_check method_reachability userFeeDidntChangeImplyNativeBalanceDidntDecrease Submited link security/certora/confs/verifyGovernance.conf-882cf9bd878a.log
GovernancePowerStrategy.conf --rule delegatePowerCompliance Submited link security/certora/confs/verifyGovernancePowerStrategy.conf-728b9eb4e723.log
GovernancePowerStrategy.conf --rule powerlessCompliance method_reachability Submited link security/certora/confs/verifyGovernancePowerStrategy.conf-988b8baf1d91.log
GovernancePowerStrategy.conf --rule transferPowerCompliance Submited link security/certora/confs/verifyGovernancePowerStrategy.conf-095e5cb4370c.log
VotingStrategy_unittests.conf Submited link security/certora/confs/verifyVotingStrategy_unittests.conf-02bf63c376f5.log

Certora Run Summary

  • Started 24 jobs
  • 0 jobs failed

Download Logs

@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 9, 2025

Certora Run Started (AAVE Governance V3 Voting Chain)

  • Group ID: 1aac6de9-b3ad-4512-bb5a-9d72ccbe0dcd
Config Status Link Log File
Legality.conf --rule createdVoteHasNonZeroHash Submited link security/certora/confs/voting/verifyLegality.conf-f5bf691e8cde.log
Legality.conf --rule legalVote Submited link security/certora/confs/voting/verifyLegality.conf-7f0b4a766259.log
Legality.conf --rule method_reachability Submited link security/certora/confs/voting/verifyLegality.conf-6425c338ade4.log
Legality.conf --rule onlyValidProposalCanChangeTally Submited link security/certora/confs/voting/verifyLegality.conf-297c016a89ee.log
Legality.conf --rule votedPowerIsImmutable Submited link security/certora/confs/voting/verifyLegality.conf-434e4331e792.log
Misc.conf Submited link security/certora/confs/voting/verifyMisc.conf-318272a01993.log
Power_summary.conf --rule method_reachability Submited link security/certora/confs/voting/verifyPower_summary.conf-da8a55a88c93.log
Power_summary.conf --rule onlyThreeTokens Submited link security/certora/confs/voting/verifyPower_summary.conf-d5242aeed663.log
Proposal_config.conf --rule createdProposalHasRoots Submited link security/certora/confs/voting/verifyProposal_config.conf-769b68bc5094.log
Proposal_config.conf --rule getProposalsConfigsDoesntRevert Submited link security/certora/confs/voting/verifyProposal_config.conf-512b44f392a8.log
Proposal_config.conf --rule method_reachability Submited link security/certora/confs/voting/verifyProposal_config.conf-b6f7094de3c5.log
Proposal_config.conf --rule proposalHasNonzeroDuration newProposalUnusedId configIsImmutable Submited link security/certora/confs/voting/verifyProposal_config.conf-8f3ecf75c43a.log
Proposal_config.conf --rule startedProposalHasConfig Submited link security/certora/confs/voting/verifyProposal_config.conf-106ef737b199.log
Proposal_states.conf --rule proposalHasNonzeroDuration method_reachability Submited link security/certora/confs/voting/verifyProposal_states.conf-2d747d5afdde.log
Proposal_states.conf --rule proposalIdIsImmutable Submited link security/certora/confs/voting/verifyProposal_states.conf-361fb180c228.log
Proposal_states.conf --rule proposalImmutability Submited link security/certora/confs/voting/verifyProposal_states.conf-707ee333ef5b.log
Proposal_states.conf --rule proposalLegalStates Submited link security/certora/confs/voting/verifyProposal_states.conf-38eb8fa10eb9.log
Proposal_states.conf --rule proposalMethodStateTransitionCompliance Submited link security/certora/confs/voting/verifyProposal_states.conf-fb1e872987dd.log
Proposal_states.conf --rule proposalTimeStateTransitionCompliance Submited link security/certora/confs/voting/verifyProposal_states.conf-ab0756ba6be4.log
Proposal_states.conf --rule startedProposalHasConfig Submited link security/certora/confs/voting/verifyProposal_states.conf-0aac118c985d.log
Proposal_states.conf --rule startsBeforeEnds Submited link security/certora/confs/voting/verifyProposal_states.conf-5b9dbf00e1ff.log
Proposal_states.conf --rule startsStrictlyBeforeEnds Submited link security/certora/confs/voting/verifyProposal_states.conf-4a743c026bd2.log
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVoteAsRepresentative_and_submitVote Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-795042468291.log
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVoteSingleProofAsRepresentative_and_submitVote Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-9554edee1635.log
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVote_and_submitVoteAsRepresentative Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-ecf2318e43a4.log
Voting_and_tally.conf --rule method_reachability Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-66502403ca52.log
Voting_and_tally.conf --rule onlyVoteCanChangeResult Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-f6a5af37c6f4.log
Voting_and_tally.conf --rule otherProposalUnchanged Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-483a9909d7ea.log
Voting_and_tally.conf --rule otherVoterUntouched Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-cee2a4c411fa.log
Voting_and_tally.conf --rule strangerVoteUnchanged Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-ae991f0fed77.log
Voting_and_tally.conf --rule sumOfVotes Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-0fbec7f8c372.log
Voting_and_tally.conf --rule voteTallyChangedOnlyByVoting Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-d408d34d76b8.log
Voting_and_tally.conf --rule voteUpdatesTally Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-b6cf2da04442.log
Voting_and_tally.conf --rule votingPowerGhostIsVotingPower Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-f75a0826669f.log
Voting_and_tally.conf --rule votingTallyCanOnlyIncrease Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-381de5175571.log

Certora Run Summary

  • Started 35 jobs
  • 0 jobs failed

Download Logs

certora-run[bot]
certora-run bot reviewed Jan 9, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: 5ef47c91-7763-42bd-9182-ab2af55e0552
Job Status Result VERIFIED Link
action_signature_immutable SUCCEEDED ✅ 2 Link
action_callData_immutable SUCCEEDED ✅ 2 Link
action_immutable_check_only_fixed_size_fields SUCCEEDED ✅ 2 Link
checkUpdateExecutors checkUpdateExecutors_witness_1 checkUpdateExecutors_witness_2 checkUpdateExecutors_witness_3 checkUpdateExecutors_witness_4 SUCCEEDED ✅ 6 Link
executedAt_is_zero_before_executed SUCCEEDED ✅ 2 Link
executed_after_queue_state_variable zero_executedAt_if_not_executed_state_variable SUCCEEDED ✅ 3 Link
action_access_level_isnt_null_after_createPayload SUCCEEDED ✅ 2 Link
delay_of_executor_of_max_access_level_within_range SUCCEEDED ✅ 2 Link
executed_when_in_queued_state executed_when_in_queued_state_variable guardian_can_cancel no_late_cancel state_variable_cant_decrease SUCCEEDED ✅ 6 Link
executor_exists_after_createPayload SUCCEEDED ✅ 2 Link
executor_exists_if_action_not_null SUCCEEDED ✅ 2 Link
executor_exists_iff_action_not_null SUCCEEDED ✅ 2 Link
executor_exists_only_if_action_not_null SUCCEEDED ✅ 2 Link
executor_isnt_used_twice executor_of_level_null_is_zero SUCCEEDED ✅ 3 Link
executor_of_maximumAccessLevelRequired_exists SUCCEEDED ✅ 2 Link
executor_of_maximumAccessLevelRequired_exists_after_createPayload SUCCEEDED ✅ 2 Link
nonempty_actions SUCCEEDED ✅ 2 Link
null_access_level_iff_state_is_none SUCCEEDED ✅ 2 Link
payload_delay_within_range SUCCEEDED ✅ 2 Link
no_early_cancellation execute_before_delay__maximumAccessLevelRequired action_immutable_fixed_size_fields initialized_payload_fields_are_immutable payload_fields_immutable_after_createPayload method_reachability SUCCEEDED ✅ 29 Link
payload_state_transition_post_state payload_state_transition_pre_state SUCCEEDED ✅ 3 Link
queuedAt_is_zero_before_queued_state_variable executedAt_is_zero_before_executed_state_variable null_state_equivalence SUCCEEDED ✅ 4 Link
zero_executedAt_if_not_executed SUCCEEDED ✅ 2 Link

certora-run[bot]
certora-run bot reviewed Jan 9, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: 46c29fa8-1dfa-4370-9ea8-ba3162040930
Job Status Result VERIFIED Link
Governance.conf --rule at_least_single_payload_active empty_payloads_iff_uninitialized_proposal SUCCEEDED ✅ 3 Link
Governance.conf --rule cannot_queue_when_voting_portal_unapproved only_owner_can_set_voting_config_witness only_owner_can_set_voting_config single_state_transition_per_block_non_creator_witness SUCCEEDED ✅ 5 Link
Governance.conf --rule check_new_representative_set_size_after_updateRepresentatives check_old_representative_set_size_after_updateRepresentatives SUCCEEDED ✅ 3 Link
Governance.conf --rule cancellationFeeZeroForFutureProposals null_state_variable_iff_null_access_level zero_voting_portal_iff_uninitialized_proposal SUCCEEDED ✅ 4 Link
esentatives_witness_antecedent_second check_new_representative_set_size_after_updateRepresentatives_witness_consequent_first check_new_representative_set_size_after_updateRepresentatives_witness_consequent_second SUCCEEDED ✅ 5 Link
Governance.conf --rule creator_is_not_zero creator_of_initialized_proposal_is_not_zero null_state_equivalence SUCCEEDED ✅ 4 Link
Governance.conf --rule immutable_after_creation_witness_access_level immutable_after_creation_witness_creation_time immutable_after_creation_witness_ipfs_hash SUCCEEDED ✅ 4 Link
VotingStrategy_unittests.conf SUCCEEDED ✅ 8 Link
Governance.conf --rule immutable_after_creation_witness_creator immutable_after_creation_witness_voting_portal SUCCEEDED ✅ 3 Link
Governance.conf --rule immutable_after_creation_witness_payload_length immutable_after_activation_witness only_state_changing_function_initiate_transitions__pre_state SUCCEEDED ✅ 4 Link
Governance.conf --rule insufficient_proposition_power_witness_time_elapsed SUCCEEDED ✅ 2 Link
Governance.conf --rule no_representative_is_zero_2 no_representative_of_zero SUCCEEDED ✅ 3 Link
Governance.conf --rule no_self_representative no_representative_is_zero consecutiveIDs totalCancellationFeeEqualETHBalance zero_address_is_not_a_valid_voting_portal SUCCEEDED ✅ 6 Link
Governance.conf --rule null_state_iff_uninitialized_proposal setInvariant addressSetInvariant SUCCEEDED ✅ 4 Link
Governance.conf --rule only_state_changing_function_initiate_transitions__post_state SUCCEEDED ✅ 2 Link
Governance.conf --rule only_valid_voting_portal_can_queue_proposal immutable_after_activation immutable_after_creation only_guardian_can_cancel guardian_can_cancel SUCCEEDED ✅ 6 Link
Governance.conf --rule proposal_voting_duration_lt_expiration_time config_voting_duration_lt_expiration_time proposal_state_transition_post_state proposal_state_transition_pre_state SUCCEEDED ✅ 5 Link
ortal_invalidate insufficient_proposition_power insufficient_proposition_power_witness_state_is_failed insufficient_proposition_power_witness_state_is_cancelled insufficient_proposition_power_witness_time_elapsed SUCCEEDED ✅ 6 Link
Governance.conf --rule single_state_transition_per_block_non_creator_non_guardian state_cant_decrease no_state_transitions_beyond_3 immutable_voting_portal SUCCEEDED ✅ 5 Link
GovernancePowerStrategy.conf --rule delegatePowerCompliance SUCCEEDED ✅ 2 Link
Governance.conf --rule state_changing_function_self_check state_variable_changing_function_self_check method_reachability userFeeDidntChangeImplyNativeBalanceDidntDecrease SUCCEEDED ✅ 5 Link
GovernancePowerStrategy.conf --rule powerlessCompliance method_reachability SUCCEEDED ✅ 3 Link
Governance.conf --rule state_changing_function_cannot_be_called_while_in_terminal_state proposal_executes_after_cooldown_period SUCCEEDED ✅ 3 Link
GovernancePowerStrategy.conf --rule transferPowerCompliance SUCCEEDED ✅ 2 Link

certora-run[bot]
certora-run bot reviewed Jan 9, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: 1aac6de9-b3ad-4512-bb5a-9d72ccbe0dcd
Job Status Result VERIFIED Link
Legality.conf --rule legalVote SUCCEEDED ✅ 2 Link
Legality.conf --rule method_reachability SUCCEEDED ✅ 2 Link
Legality.conf --rule createdVoteHasNonZeroHash SUCCEEDED ✅ 2 Link
Legality.conf --rule onlyValidProposalCanChangeTally SUCCEEDED ✅ 2 Link
Legality.conf --rule votedPowerIsImmutable SUCCEEDED ✅ 2 Link
Misc.conf SUCCEEDED ✅ 6 Link
Proposal_config.conf --rule createdProposalHasRoots SUCCEEDED ✅ 2 Link
Proposal_config.conf --rule getProposalsConfigsDoesntRevert SUCCEEDED ✅ 2 Link
Power_summary.conf --rule method_reachability SUCCEEDED ✅ 2 Link
Power_summary.conf --rule onlyThreeTokens SUCCEEDED ✅ 2 Link
Proposal_config.conf --rule proposalHasNonzeroDuration newProposalUnusedId configIsImmutable SUCCEEDED ✅ 4 Link
Proposal_config.conf --rule method_reachability SUCCEEDED ✅ 2 Link
Proposal_config.conf --rule startedProposalHasConfig SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalIdIsImmutable SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalHasNonzeroDuration method_reachability SUCCEEDED ✅ 3 Link
Proposal_states.conf --rule proposalImmutability SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalLegalStates SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalMethodStateTransitionCompliance SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalTimeStateTransitionCompliance SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule startedProposalHasConfig SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule startsBeforeEnds SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule startsStrictlyBeforeEnds SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVoteAsRepresentative_and_submitVote SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVoteSingleProofAsRepresentative_and_submitVote SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVote_and_submitVoteAsRepresentative SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule method_reachability SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule otherProposalUnchanged SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule onlyVoteCanChangeResult SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule otherVoterUntouched SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule strangerVoteUnchanged SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule sumOfVotes SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule votingPowerGhostIsVotingPower SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule voteTallyChangedOnlyByVoting SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule voteUpdatesTally SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule votingTallyCanOnlyIncrease SUCCEEDED ✅ 2 Link

@H00N24 H00N24 requested a review from shellygr January 9, 2025 08:26
@github-actions GitHub Actions
Copy link

Certora Run Started (AAVE Governance V3 Mainnet)

  • Group ID: 0da4aa8e-b5e8-4c42-91d0-f7ed98ecdcf7
Config Status Link Log File
Governance.conf --rule at_least_single_payload_active empty_payloads_iff_uninitialized_proposal Submited link security/certora/confs/verifyGovernance.conf-b09ef002b945.log
Governance.conf --rule cancellationFeeZeroForFutureProposals null_state_variable_iff_null_access_level zero_voting_portal_iff_uninitialized_proposal Submited link security/certora/confs/verifyGovernance.conf-8867f3388b8d.log
Governance.conf --rule cannot_queue_when_voting_portal_unapproved only_owner_can_set_voting_config_witness only_owner_can_set_voting_config single_state_transition_per_block_non_creator_witness Submited link security/certora/confs/verifyGovernance.conf-0b57db2a242e.log
Governance.conf --rule check_new_representative_set_size_after_updateRepresentatives check_old_representative_set_size_after_updateRepresentatives Submited link security/certora/confs/verifyGovernance.conf-e2e1593f288e.log
Governance.conf --rule check_new_representative_set_size_after_updateRepresentatives_witness_antecedent_first check_new_representative_set_size_after_updateRepresentatives_witness_antecedent_second check_new_representative_set_size_after_updateRepresentatives_witness_consequent_first check_new_representative_set_size_after_updateRepresentatives_witness_consequent_second Submited link security/certora/confs/verifyGovernance.conf-68d601f255e5.log
Governance.conf --rule creator_is_not_zero creator_of_initialized_proposal_is_not_zero null_state_equivalence Submited link security/certora/confs/verifyGovernance.conf-d90a4c8043e3.log
Governance.conf --rule immutable_after_creation_witness_access_level immutable_after_creation_witness_creation_time immutable_after_creation_witness_ipfs_hash Submited link security/certora/confs/verifyGovernance.conf-d6ac7060bd42.log
Governance.conf --rule immutable_after_creation_witness_creator immutable_after_creation_witness_voting_portal Submited link security/certora/confs/verifyGovernance.conf-1c14025b756f.log
Governance.conf --rule immutable_after_creation_witness_payload_length immutable_after_activation_witness only_state_changing_function_initiate_transitions__pre_state Submited link security/certora/confs/verifyGovernance.conf-652816e6df1e.log
Governance.conf --rule insufficient_proposition_power_witness_time_elapsed Submited link security/certora/confs/verifyGovernance.conf-ae84bfb6b5ea.log
Governance.conf --rule no_representative_is_zero_2 no_representative_of_zero Submited link security/certora/confs/verifyGovernance.conf-c6853828da8d.log
Governance.conf --rule no_self_representative no_representative_is_zero consecutiveIDs totalCancellationFeeEqualETHBalance zero_address_is_not_a_valid_voting_portal Submited link security/certora/confs/verifyGovernance.conf-9f713c4f2d59.log
Governance.conf --rule null_state_iff_uninitialized_proposal setInvariant addressSetInvariant Submited link security/certora/confs/verifyGovernance.conf-06673181361f.log
Governance.conf --rule only_state_changing_function_initiate_transitions__post_state Submited link security/certora/confs/verifyGovernance.conf-4a988496aa71.log
Governance.conf --rule only_valid_voting_portal_can_queue_proposal immutable_after_activation immutable_after_creation only_guardian_can_cancel guardian_can_cancel Submited link security/certora/confs/verifyGovernance.conf-ae6e0767d6a3.log
Governance.conf --rule proposal_after_voting_portal_invalidate insufficient_proposition_power insufficient_proposition_power_witness_state_is_failed insufficient_proposition_power_witness_state_is_cancelled insufficient_proposition_power_witness_time_elapsed Submited link security/certora/confs/verifyGovernance.conf-6a59d1a4a71e.log
Governance.conf --rule proposal_voting_duration_lt_expiration_time config_voting_duration_lt_expiration_time proposal_state_transition_post_state proposal_state_transition_pre_state Submited link security/certora/confs/verifyGovernance.conf-e49f4f17bf5a.log
Governance.conf --rule single_state_transition_per_block_non_creator_non_guardian state_cant_decrease no_state_transitions_beyond_3 immutable_voting_portal Submited link security/certora/confs/verifyGovernance.conf-1617bb1628a5.log
Governance.conf --rule state_changing_function_cannot_be_called_while_in_terminal_state proposal_executes_after_cooldown_period Submited link security/certora/confs/verifyGovernance.conf-52f12f899073.log
Governance.conf --rule state_changing_function_self_check state_variable_changing_function_self_check method_reachability userFeeDidntChangeImplyNativeBalanceDidntDecrease Submited link security/certora/confs/verifyGovernance.conf-a9ee990aab41.log
GovernancePowerStrategy.conf --rule delegatePowerCompliance Submited link security/certora/confs/verifyGovernancePowerStrategy.conf-855c3a7cb191.log
GovernancePowerStrategy.conf --rule powerlessCompliance method_reachability Submited link security/certora/confs/verifyGovernancePowerStrategy.conf-855a5fe78ef2.log
GovernancePowerStrategy.conf --rule transferPowerCompliance Submited link security/certora/confs/verifyGovernancePowerStrategy.conf-04c3a1647333.log
VotingStrategy_unittests.conf Submited link security/certora/confs/verifyVotingStrategy_unittests.conf-8973e841eacc.log

Certora Run Summary

  • Started 24 jobs
  • 0 jobs failed

Download Logs

@github-actions GitHub Actions
Copy link

Certora Run Started (AAVE Governance V3 Execution Chain)

  • Group ID: 8bb486d1-0f96-4e4d-8da9-cfc071c48a23
Config Status Link Log File
action_access_level_isnt_null_after_createPayload Submited link security/certora/confs/payloads/verifyPayloadsController.conf-2e169d6b0dc8.log
action_callData_immutable Submited link security/certora/confs/payloads/verifyPayloadsController.conf-c5028c6016a3.log
action_immutable_check_only_fixed_size_fields Submited link security/certora/confs/payloads/verifyPayloadsController.conf-4acc7c219048.log
action_signature_immutable Submited link security/certora/confs/payloads/verifyPayloadsController.conf-3f7c93eb53da.log
checkUpdateExecutors checkUpdateExecutors_witness_1 checkUpdateExecutors_witness_2 checkUpdateExecutors_witness_3 checkUpdateExecutors_witness_4 Submited link security/certora/confs/payloads/verifyPayloadsController.conf-ebd9a10bcac0.log
delay_of_executor_of_max_access_level_within_range Submited link security/certora/confs/payloads/verifyPayloadsController.conf-a60b8ebbc7dd.log
executedAt_is_zero_before_executed Submited link security/certora/confs/payloads/verifyPayloadsController.conf-cfbc7a631a4c.log
executed_after_queue_state_variable zero_executedAt_if_not_executed_state_variable Submited link security/certora/confs/payloads/verifyPayloadsController.conf-3fa6f259c113.log
executed_when_in_queued_state executed_when_in_queued_state_variable guardian_can_cancel no_late_cancel state_variable_cant_decrease Submited link security/certora/confs/payloads/verifyPayloadsController.conf-ad4149ebde7b.log
executor_exists_after_createPayload Submited link security/certora/confs/payloads/verifyPayloadsController.conf-d57dcfeac1e7.log
executor_exists_if_action_not_null Submited link security/certora/confs/payloads/verifyPayloadsController.conf-46dd2265c88b.log
executor_exists_iff_action_not_null Submited link security/certora/confs/payloads/verifyPayloadsController.conf-d5b13eead529.log
executor_exists_only_if_action_not_null Submited link security/certora/confs/payloads/verifyPayloadsController.conf-d1e8d4aa8535.log
executor_isnt_used_twice executor_of_level_null_is_zero Submited link security/certora/confs/payloads/verifyPayloadsController.conf-c8d08b72c8fb.log
executor_of_maximumAccessLevelRequired_exists Submited link security/certora/confs/payloads/verifyPayloadsController.conf-9b19bbaea441.log
executor_of_maximumAccessLevelRequired_exists_after_createPayload Submited link security/certora/confs/payloads/verifyPayloadsController.conf-8bce2e1c3d12.log
nonempty_actions Submited link security/certora/confs/payloads/verifyPayloadsController.conf-88b268d958f2.log
null_access_level_iff_state_is_none Submited link security/certora/confs/payloads/verifyPayloadsController.conf-fe1803143622.log
payload_delay_within_range Submited link security/certora/confs/payloads/verifyPayloadsController.conf-34040fbda4f4.log
payload_maximal_access_level_gt_action_access_level state_cant_decrease no_transition_beyond_state_gt_3 no_transition_beyond_state_variable_gt_3 no_queue_after_expiration empty_actions_if_out_of_bound_payload expirationTime_equal_to_createAt_plus_EXPIRATION_DELAY empty_actions_iff_uninitialized null_access_level_if_out_of_bound_payload null_creator_and_zero_expiration_time_if_out_of_bound_payload empty_actions_only_if_uninitialized_payload executor_access_level_within_range consecutiveIDs empty_actions_if_uninitialized_payload queued_before_expiration_delay payload_grace_period_eq_global_grace_period null_access_level_only_if_out_of_bound_payload null_state_variable_if_out_of_bound_payload created_in_the_past queued_after_created executed_after_queue queuedAt_is_zero_before_queued no_early_cancellation execute_before_delay__maximumAccessLevelRequired action_immutable_fixed_size_fields initialized_payload_fields_are_immutable payload_fields_immutable_after_createPayload method_reachability Submited link security/certora/confs/payloads/verifyPayloadsController.conf-5021143bf8b5.log
payload_state_transition_post_state payload_state_transition_pre_state Submited link security/certora/confs/payloads/verifyPayloadsController.conf-b8c4e9332550.log
queuedAt_is_zero_before_queued_state_variable executedAt_is_zero_before_executed_state_variable null_state_equivalence Submited link security/certora/confs/payloads/verifyPayloadsController.conf-27c10483ec27.log
zero_executedAt_if_not_executed Submited link security/certora/confs/payloads/verifyPayloadsController.conf-3cc335ca76a4.log

Certora Run Summary

  • Started 23 jobs
  • 0 jobs failed

Download Logs

@github-actions GitHub Actions
Copy link

Certora Run Started (AAVE Governance V3 Voting Chain)

  • Group ID: ff010ef0-7bb7-4998-856d-f0b739d39382
Config Status Link Log File
Legality.conf --rule createdVoteHasNonZeroHash Submited link security/certora/confs/voting/verifyLegality.conf-0a6acdad46bf.log
Legality.conf --rule legalVote Submited link security/certora/confs/voting/verifyLegality.conf-6b434ecc4104.log
Legality.conf --rule method_reachability Submited link security/certora/confs/voting/verifyLegality.conf-1be30a54e133.log
Legality.conf --rule onlyValidProposalCanChangeTally Submited link security/certora/confs/voting/verifyLegality.conf-c2010031136b.log
Legality.conf --rule votedPowerIsImmutable Submited link security/certora/confs/voting/verifyLegality.conf-b6212fb7cb59.log
Misc.conf Submited link security/certora/confs/voting/verifyMisc.conf-822d9f539cdd.log
Power_summary.conf --rule method_reachability Submited link security/certora/confs/voting/verifyPower_summary.conf-f7e0e3b32ed7.log
Power_summary.conf --rule onlyThreeTokens Submited link security/certora/confs/voting/verifyPower_summary.conf-792d7a45f446.log
Proposal_config.conf --rule createdProposalHasRoots Submited link security/certora/confs/voting/verifyProposal_config.conf-ae50cd56b01c.log
Proposal_config.conf --rule getProposalsConfigsDoesntRevert Submited link security/certora/confs/voting/verifyProposal_config.conf-e58e9dfe4f5d.log
Proposal_config.conf --rule method_reachability Submited link security/certora/confs/voting/verifyProposal_config.conf-798f8f8fb0c8.log
Proposal_config.conf --rule proposalHasNonzeroDuration newProposalUnusedId configIsImmutable Submited link security/certora/confs/voting/verifyProposal_config.conf-260223aa8ada.log
Proposal_config.conf --rule startedProposalHasConfig Submited link security/certora/confs/voting/verifyProposal_config.conf-5e4ba9b5dd61.log
Proposal_states.conf --rule proposalHasNonzeroDuration method_reachability Submited link security/certora/confs/voting/verifyProposal_states.conf-673825a5ab91.log
Proposal_states.conf --rule proposalIdIsImmutable Submited link security/certora/confs/voting/verifyProposal_states.conf-4d13ad654150.log
Proposal_states.conf --rule proposalImmutability Submited link security/certora/confs/voting/verifyProposal_states.conf-0957431177e5.log
Proposal_states.conf --rule proposalLegalStates Submited link security/certora/confs/voting/verifyProposal_states.conf-89cb9eaa7c0b.log
Proposal_states.conf --rule proposalMethodStateTransitionCompliance Submited link security/certora/confs/voting/verifyProposal_states.conf-0e4893dfecbe.log
Proposal_states.conf --rule proposalTimeStateTransitionCompliance Submited link security/certora/confs/voting/verifyProposal_states.conf-92bd27db1b5a.log
Proposal_states.conf --rule startedProposalHasConfig Submited link security/certora/confs/voting/verifyProposal_states.conf-ed2cf130aad2.log
Proposal_states.conf --rule startsBeforeEnds Submited link security/certora/confs/voting/verifyProposal_states.conf-62b37ef29f6d.log
Proposal_states.conf --rule startsStrictlyBeforeEnds Submited link security/certora/confs/voting/verifyProposal_states.conf-c156c77aa167.log
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVoteAsRepresentative_and_submitVote Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-b146cf4f9a42.log
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVoteSingleProofAsRepresentative_and_submitVote Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-8c17f1f90b34.log
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVote_and_submitVoteAsRepresentative Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-a17e1e33cd80.log
Voting_and_tally.conf --rule method_reachability Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-5c368d44ff29.log
Voting_and_tally.conf --rule onlyVoteCanChangeResult Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-6740944c8c52.log
Voting_and_tally.conf --rule otherProposalUnchanged Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-c8b55d571092.log
Voting_and_tally.conf --rule otherVoterUntouched Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-d6b82fb99ec4.log
Voting_and_tally.conf --rule strangerVoteUnchanged Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-dc97b5c4a0ca.log
Voting_and_tally.conf --rule sumOfVotes Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-a04213755584.log
Voting_and_tally.conf --rule voteTallyChangedOnlyByVoting Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-8484e4ec8f1f.log
Voting_and_tally.conf --rule voteUpdatesTally Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-7373c75c94d7.log
Voting_and_tally.conf --rule votingPowerGhostIsVotingPower Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-280b7bebd056.log
Voting_and_tally.conf --rule votingTallyCanOnlyIncrease Submited link security/certora/confs/voting/verifyVoting_and_tally.conf-b3a192c53b42.log

Certora Run Summary

  • Started 35 jobs
  • 0 jobs failed

Download Logs

certora-run[bot]
certora-run bot reviewed Jan 24, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: 8bb486d1-0f96-4e4d-8da9-cfc071c48a23
Job Status Result VERIFIED Link
action_access_level_isnt_null_after_createPayload SUCCEEDED ✅ 2 Link
action_immutable_check_only_fixed_size_fields SUCCEEDED ✅ 2 Link
action_callData_immutable SUCCEEDED ✅ 2 Link
action_signature_immutable SUCCEEDED ✅ 2 Link
checkUpdateExecutors checkUpdateExecutors_witness_1 checkUpdateExecutors_witness_2 checkUpdateExecutors_witness_3 checkUpdateExecutors_witness_4 SUCCEEDED ✅ 6 Link
executedAt_is_zero_before_executed SUCCEEDED ✅ 2 Link
delay_of_executor_of_max_access_level_within_range SUCCEEDED ✅ 2 Link
executed_after_queue_state_variable zero_executedAt_if_not_executed_state_variable SUCCEEDED ✅ 3 Link
executed_when_in_queued_state executed_when_in_queued_state_variable guardian_can_cancel no_late_cancel state_variable_cant_decrease SUCCEEDED ✅ 6 Link
executor_exists_after_createPayload SUCCEEDED ✅ 2 Link
executor_exists_if_action_not_null SUCCEEDED ✅ 2 Link
executor_exists_only_if_action_not_null SUCCEEDED ✅ 2 Link
executor_exists_iff_action_not_null SUCCEEDED ✅ 2 Link
executor_isnt_used_twice executor_of_level_null_is_zero SUCCEEDED ✅ 3 Link
executor_of_maximumAccessLevelRequired_exists SUCCEEDED ✅ 2 Link
executor_of_maximumAccessLevelRequired_exists_after_createPayload SUCCEEDED ✅ 2 Link
null_access_level_iff_state_is_none SUCCEEDED ✅ 2 Link
nonempty_actions SUCCEEDED ✅ 2 Link
no_early_cancellation execute_before_delay__maximumAccessLevelRequired action_immutable_fixed_size_fields initialized_payload_fields_are_immutable payload_fields_immutable_after_createPayload method_reachability SUCCEEDED ✅ 29 Link
payload_delay_within_range SUCCEEDED ✅ 2 Link
payload_state_transition_post_state payload_state_transition_pre_state SUCCEEDED ✅ 3 Link
queuedAt_is_zero_before_queued_state_variable executedAt_is_zero_before_executed_state_variable null_state_equivalence SUCCEEDED ✅ 4 Link
zero_executedAt_if_not_executed SUCCEEDED ✅ 2 Link

certora-run[bot]
certora-run bot reviewed Jan 24, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: 0da4aa8e-b5e8-4c42-91d0-f7ed98ecdcf7
Job Status Result VERIFIED Link
Governance.conf --rule cancellationFeeZeroForFutureProposals null_state_variable_iff_null_access_level zero_voting_portal_iff_uninitialized_proposal SUCCEEDED ✅ 4 Link
Governance.conf --rule at_least_single_payload_active empty_payloads_iff_uninitialized_proposal SUCCEEDED ✅ 3 Link
Governance.conf --rule cannot_queue_when_voting_portal_unapproved only_owner_can_set_voting_config_witness only_owner_can_set_voting_config single_state_transition_per_block_non_creator_witness SUCCEEDED ✅ 5 Link
Governance.conf --rule check_new_representative_set_size_after_updateRepresentatives check_old_representative_set_size_after_updateRepresentatives SUCCEEDED ✅ 3 Link
esentatives_witness_antecedent_second check_new_representative_set_size_after_updateRepresentatives_witness_consequent_first check_new_representative_set_size_after_updateRepresentatives_witness_consequent_second SUCCEEDED ✅ 5 Link
Governance.conf --rule creator_is_not_zero creator_of_initialized_proposal_is_not_zero null_state_equivalence SUCCEEDED ✅ 4 Link
VotingStrategy_unittests.conf SUCCEEDED ✅ 8 Link
Governance.conf --rule immutable_after_creation_witness_access_level immutable_after_creation_witness_creation_time immutable_after_creation_witness_ipfs_hash SUCCEEDED ✅ 4 Link
Governance.conf --rule immutable_after_creation_witness_creator immutable_after_creation_witness_voting_portal SUCCEEDED ✅ 3 Link
Governance.conf --rule immutable_after_creation_witness_payload_length immutable_after_activation_witness only_state_changing_function_initiate_transitions__pre_state SUCCEEDED ✅ 4 Link
Governance.conf --rule insufficient_proposition_power_witness_time_elapsed SUCCEEDED ✅ 2 Link
Governance.conf --rule no_self_representative no_representative_is_zero consecutiveIDs totalCancellationFeeEqualETHBalance zero_address_is_not_a_valid_voting_portal SUCCEEDED ✅ 6 Link
Governance.conf --rule no_representative_is_zero_2 no_representative_of_zero SUCCEEDED ✅ 3 Link
Governance.conf --rule null_state_iff_uninitialized_proposal setInvariant addressSetInvariant SUCCEEDED ✅ 4 Link
Governance.conf --rule only_state_changing_function_initiate_transitions__post_state SUCCEEDED ✅ 2 Link
ortal_invalidate insufficient_proposition_power insufficient_proposition_power_witness_state_is_failed insufficient_proposition_power_witness_state_is_cancelled insufficient_proposition_power_witness_time_elapsed SUCCEEDED ✅ 6 Link
Governance.conf --rule proposal_voting_duration_lt_expiration_time config_voting_duration_lt_expiration_time proposal_state_transition_post_state proposal_state_transition_pre_state SUCCEEDED ✅ 5 Link
GovernancePowerStrategy.conf --rule delegatePowerCompliance SUCCEEDED ✅ 2 Link
Governance.conf --rule state_changing_function_cannot_be_called_while_in_terminal_state proposal_executes_after_cooldown_period SUCCEEDED ✅ 3 Link
Governance.conf --rule single_state_transition_per_block_non_creator_non_guardian state_cant_decrease no_state_transitions_beyond_3 immutable_voting_portal SUCCEEDED ✅ 5 Link
GovernancePowerStrategy.conf --rule powerlessCompliance method_reachability SUCCEEDED ✅ 3 Link
Governance.conf --rule state_changing_function_self_check state_variable_changing_function_self_check method_reachability userFeeDidntChangeImplyNativeBalanceDidntDecrease SUCCEEDED ✅ 5 Link
GovernancePowerStrategy.conf --rule transferPowerCompliance SUCCEEDED ✅ 2 Link
Governance.conf --rule only_valid_voting_portal_can_queue_proposal immutable_after_activation immutable_after_creation only_guardian_can_cancel guardian_can_cancel SUCCEEDED ✅ 6 Link

certora-run[bot]
certora-run bot reviewed Jan 24, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: ff010ef0-7bb7-4998-856d-f0b739d39382
Job Status Result VERIFIED Link
Legality.conf --rule legalVote SUCCEEDED ✅ 2 Link
Legality.conf --rule createdVoteHasNonZeroHash SUCCEEDED ✅ 2 Link
Legality.conf --rule method_reachability SUCCEEDED ✅ 2 Link
Legality.conf --rule onlyValidProposalCanChangeTally SUCCEEDED ✅ 2 Link
Legality.conf --rule votedPowerIsImmutable SUCCEEDED ✅ 2 Link
Misc.conf SUCCEEDED ✅ 6 Link
Power_summary.conf --rule method_reachability SUCCEEDED ✅ 2 Link
Proposal_config.conf --rule createdProposalHasRoots SUCCEEDED ✅ 2 Link
Proposal_config.conf --rule getProposalsConfigsDoesntRevert SUCCEEDED ✅ 2 Link
Power_summary.conf --rule onlyThreeTokens SUCCEEDED ✅ 2 Link
Proposal_config.conf --rule method_reachability SUCCEEDED ✅ 2 Link
Proposal_config.conf --rule proposalHasNonzeroDuration newProposalUnusedId configIsImmutable SUCCEEDED ✅ 4 Link
Proposal_config.conf --rule startedProposalHasConfig SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalHasNonzeroDuration method_reachability SUCCEEDED ✅ 3 Link
Proposal_states.conf --rule proposalImmutability SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalIdIsImmutable SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalLegalStates SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalMethodStateTransitionCompliance SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalTimeStateTransitionCompliance SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule startedProposalHasConfig SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule startsBeforeEnds SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule startsStrictlyBeforeEnds SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVoteAsRepresentative_and_submitVote SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVoteSingleProofAsRepresentative_and_submitVote SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVote_and_submitVoteAsRepresentative SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule method_reachability SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule onlyVoteCanChangeResult SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule otherProposalUnchanged SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule otherVoterUntouched SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule strangerVoteUnchanged SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule sumOfVotes SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule voteTallyChangedOnlyByVoting SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule votingTallyCanOnlyIncrease SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule voteUpdatesTally SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule votingPowerGhostIsVotingPower SUCCEEDED ✅ 2 Link

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@certora-run certora-run[bot] certora-run[bot] left review comments

@MichaelMorami MichaelMorami Awaiting requested review from MichaelMorami

@yoav-el-certora yoav-el-certora Awaiting requested review from yoav-el-certora

@shellygr shellygr Awaiting requested review from shellygr

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@H00N24