Skip to content

Formal verification of Account (7702+7579) #5872

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
Merged
merged 27 commits into from
Aug 21, 2025
Merged

Formal verification of Account (7702+7579) #5872

merged 27 commits into from
Aug 21, 2025

Conversation

Amxx
Copy link
Collaborator

@Amxx Amxx commented Aug 21, 2025

Replaces #5785

Amxx and others added 23 commits July 6, 2025 18:46
@Amxx
Formal verification of Account (7702+7579)
6273cb9
@Amxx
fix script
ec0e4e8
@Amxx
check value passed
9b38876
@Amxx
up
3c0c43d
@Amxx
up
139373f
@Amxx
up
3a7078b
@Amxx
finally a solution for the fallback issue (needs patch)
cd8d1e8
@Amxx
minimize change
6f2e783
@Amxx
add rule
ea59b14
@Amxx
specifications for module install / uninstall
7292782
@Amxx
use invariants to certify storage consistency
896e1a3
@Amxx
use persistent ghost
8a52823
@Amxx
check selectors
5f95425
@Amxx
Update
eee46c1 
https://prover.certora.com/output/71959/bcce84865f864eafaf7d9dd6388d4136?anonymousKey=5b892739b94fc58e0168193c3f232939c4765d3b
@Amxx
Check possibility of multiple call/delegatecall
f4d6bbb 
https://prover.certora.com/output/71959/9316d0908b9e4f669bfec8b807d47e7a?anonymousKey=0b0e88cf1315090a34ac484f09553dbc8d0d28c7
@Amxx
Merge branch 'master' into FV/account
aacd75c
@ernestognw
Update solc version
8347f1e
@Amxx
update fv-requirements
a6ecba8
@Amxx
make report public
de0a6b2
@Amxx
helpers
101f417
@Amxx
Merge branch 'master' into FV/account
b50a27f
@Amxx
address dirty storage issue
11ee939
@Amxx
indentation
7a99c91
@Amxx Amxx requested a review from a team as a code owner August 21, 2025 15:02
@changeset-bot changeset-bot
Copy link

changeset-bot bot commented Aug 21, 2025 •
edited
Loading

⚠️ No Changeset found

Latest commit: 8a3b496

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

ernestognw
ernestognw previously approved these changes Aug 21, 2025
View reviewed changes
Copy link
Member

@ernestognw ernestognw left a comment

Choose a reason for hiding this comment

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

Left some nits, I'll see if I can make it work but LGTM

@Amxx @ernestognw
Update certora/specs/Account.spec
179040d 
Co-authored-by: Ernesto García <[email protected]>
@Amxx Amxx merged commit 7eb34c4 into master Aug 21, 2025
21 checks passed
@Amxx Amxx deleted the FV/account branch August 21, 2025 21:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ernestognw ernestognw ernestognw approved these changes

Assignees
No one assigned
Labels
Account Abstraction formal-verification Enable FV run in a PR. ignore-changeset
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@Amxx @ernestognw