safe-global / safe-contracts

93%

main: 94%

LAST BUILD ON BRANCH certora/moduleExecutionRule

branch: certora/moduleExecutionRule

CHANGE BRANCH

x

Reset

• certora/moduleExecutionRule
• 1.3.0-libs.0
• ISafe
• add-network-configs
• add-precommit
• add_tests_eip1271
• bounty/nonce_reorder
• bounty_module_pagination
• bug/certora-unresolved-setup-fix
• bug/comment-typo
• bug/execTransactionFromModuleReturnData-mit-guard
• certora/check-owners-list-consistency
• certora/cleanup
• certora/guard-update
• certora/handler
• certora/module-additions
• certora/mutation-testing
• certora/native-balance-update
• certora/rule-uniq-owners
• certora/safe-is-setup
• certora/signatures-rule-options-fix
• certora/signed-messages
• certora/singleton-address-doesnt-change
• certora/spec2
• certora/treshold-ownercount
• certora/update-nonce-monotonicity-rule
• certora/v6-spec-update
• certora/verify-monotonicity-for-havocs
• certoraOwnerReach
• change-cla-permissions
• checkSignatures
• chore/benchmark-typo
• chore/coverage-skip-test
• chore/javascript-formatting
• chore/prettier-shenanigans
• chore/remove-outdated-networks
• chore/version-pamp
• chore/version-pamp-141
• ci/pin-certora
• ci/pin-certora-proper-parallel-coverage
• cla-signatures
• contract-size
• dependabot/npm_and_yarn/axios-0.21.4
• dependabot/npm_and_yarn/cookiejar-2.1.4
• dependabot/npm_and_yarn/cross-fetch-2.2.6
• dependabot/npm_and_yarn/decode-uri-component-0.2.2
• dependabot/npm_and_yarn/express-4.18.2
• dependabot/npm_and_yarn/flat-and-eth-gas-reporter-and-solidity-coverage-5.0.2
• dependabot/npm_and_yarn/follow-redirects-1.15.4
• dependabot/npm_and_yarn/http-cache-semantics-4.1.1
• dependabot/npm_and_yarn/qs-6.5.3
• dependabot/npm_and_yarn/simple-get-2.8.2
• dependabot/npm_and_yarn/tough-cookie-and-eth-gas-reporter--removed
• dependabot/npm_and_yarn/undici-5.19.1
• dependabot/npm_and_yarn/undici-5.26.3
• dependabot/npm_and_yarn/word-wrap-1.2.4
• deps-bump
• deps/upgrade
• docs/1.5.0-changelog
• docs/audit-notes-2
• docs/audit-notes-4
• docs/fix-return-comment
• docs/general-overview-of-safe
• docs/improve-natspec-docs
• docs/improve-natspec-docs-2
• docs/improve-natspec-docs-3
• docs/improve-natspec-docs-4
• docs/improve-natspec-docs-5
• docs/improve-natspec-docs-6
• docs/improve-natspec-docs-7
• error_codes_enhanced
• experiment/eip4337
• experimental_fix_the_x
• feat/audit-notes
• feat/audit-notes-1
• feat/eip-165-test
• feat/external-contract-signature
• feat/fbhandler-exploit
• feat/improve-proxy-factory
• feat/index-addresses-events
• feat/memory-safe-assembly
• feat/multisend-self-tests
• feat/proxycreated-indexed-proxyaddress
• feat/remove-gasleft
• feat/remove-requiredtxgas
• feat/remove-transfer-send
• feat/remove-transfer-send-2
• feat/signature-decoder-optimization
• feat/universal-onlyowner-module
• feat/use-interface-in-compatfbhandler
• feat/use-safe-singleton-factory
• feature-719-rename-repository
• feature/1.4.0-deployment
• feature/1.4.1-migration
• feature/1.4.1-migration-enhancements
• feature/1.5.0-migration
• feature/bytecode-shaving-2
• feature/checknsignatures-datahash
• feature/documentation
• feature/gnosissafe-safe
• feature/module-guard
• feature/module-tx-alternative-impl
• feature/module-tx-guard
• feature/optimize-onlyowners-guard
• feature/remove-bytes-from-checksignatures
• feature/remove-name-version
• feature/setupmodules-check-to-is-a-contract
• feature/simplify-test4337fallbackhandler
• feature/update_safe_references
• fix-local-verify
• fix/certora-ci
• fix/eip1271-validation
• fix/error_code_typo
• fix/gasleft-setupModules
• fix/js-bundle
• fix/linter-warnings
• fix/module-manager-comment
• fix/safe-inheritance-order
• fix/typescript-setup
• fix1271-wip
• fix_changelog
• formal-verification
• fv/adjust-execTransactionRule
• fv/checkSignatures
• fv/moduleReach
• main
• migrate-l2
• migrate-l2-111
• mmv08-patch-1
• optimizer-enabled
• optimizer-enabled-with-original-solc
• pin-certora-cli-version
• refactor/make-base-contracts-abstract
• refactor/rename-defaultfallbackhandler
• refactor/rename-ether-fallback
• refs/heads/certora/native-balance-update
• refs/heads/certora/update-nonce-monotonicity-rule
• refs/heads/chore/version-pamp-141
• refs/heads/fix/typescript-setup
• refs/heads/main
• refs/tags/v1.4.0
• refs/tags/v1.4.1
• refs/tags/v1.4.1-build.0
• release-branch/v1.4.1
• release/1.4.1
• release/v1.5.0
• setup_clas
• slither-graphs
• test-checknsigs
• tests-correction
• update-cla
• update-readme-npm-badge
• use-new-safe-singleton-factory
• v1.4.1/js-bundle-fix
• v1_3_0_zksync
• wip-eip-1271-fix
• zksync

Build # 6013168516

Build Type

Pull #648

github

Committed by mmv08

Commit Message

add a rule for module transaction executions

Pull Request Pull Request #648: Formal verification: Add rules that check only modules can execute module transactions

Run Details

194 of 214 branches covered (0.0%)

Branch coverage included in aggregate %.

320 of 340 relevant lines covered (94.12%)

103.49 hits per line