Skip to content
Navigation Menu
Sign in
Appearance settings
Platform
AI CODE CREATION
GitHub Copilot
Write better code with AI
GitHub Copilot app
Direct agents from issue to merge
MCP Registry
Integrate external tools
DEVELOPER WORKFLOWS
Actions
Automate any workflow
Codespaces
Instant dev environments
Issues
Plan and track work
Code Review
Manage code changes
Code Quality
Enforce quality at merge
APPLICATION SECURITY
GitHub Advanced Security
Find and fix vulnerabilities
Code security
Secure your code as you build
Secret protection
Stop leaks before they start
EXPLORE
Why GitHub
Documentation
Blog
Changelog
Marketplace
View all features
Solutions
BY COMPANY SIZE
Enterprises
Small and medium teams
Startups
Nonprofits
BY USE CASE
App Modernization
DevSecOps
DevOps
CI/CD
View all use cases
BY INDUSTRY
Healthcare
Financial services
Manufacturing
Government
View all industries
View all solutions
Resources
EXPLORE BY TOPIC
AI
Software Development
DevOps
Security
View all topics
EXPLORE BY TYPE
Customer stories
Events & webinars
Ebooks & reports
Business insights
GitHub Skills
SUPPORT & SERVICES
Documentation
Customer support
Community forum
Trust center
Partners
View all resources
Open Source
COMMUNITY
GitHub Sponsors
Fund open source developers
PROGRAMS
Security Lab
Maintainer Community
GitHub Stars
Archive Program
REPOSITORIES
Topics
Trending
Collections
Enterprise
ENTERPRISE SOLUTIONS
Enterprise platform
AI-powered developer platform
AVAILABLE ADD-ONS
GitHub Advanced Security
Enterprise-grade security features
Copilot for Business
Enterprise-grade AI features
Premium Support
Enterprise-grade 24/7 support
Pricing
Search
/
Sign in
Sign up
Appearance settings
You signed in with another tab or window.
Reload
to refresh your session.
You signed out in another tab or window.
Reload
to refresh your session.
You switched accounts on another tab or window.
Reload
to refresh your session.
Dismiss alert
{{ message }}
OpenZeppelin
/
openzeppelin-contracts
Public
Notifications
You must be signed in to change notification settings
Fork
12.4k
Star
27.3k
Code
Issues
214
Pull requests
143
Actions
Security and quality
20
Insights
Additional navigation options
Code
Issues
Pull requests
Actions
Security and quality
Insights
Add formal verification for ERC-4626
- #6724
#6724
Open
EperezOk
wants to merge 20 commits into
OpenZeppelin:master
OpenZeppelin/openzeppelin-contracts:master
from
EperezOk:fv/erc4626-certora
EperezOk/openzeppelin-contracts:fv/erc4626-certora
Copy head branch name to clipboard
Conversation
Commits
20
(20)
Checks
Files changed
Open
Add formal verification for ERC-4626
#6724
EperezOk
wants to merge 20 commits into
OpenZeppelin:master
OpenZeppelin/openzeppelin-contracts:master
from
EperezOk:fv/erc4626-certora
EperezOk/openzeppelin-contracts:fv/erc4626-certora
Copy head branch name to clipboard
Commits
Commits on Sep 28, 2026
fv: add ERC4626 harness skeleton
Show description for ffc2c47
EperezOk
and
claude
committed
ffc2c47
View commit details
Copy full SHA for ffc2c47
Browse repository at this point
fv: add ERC4626 summary layer and smoke rules
Show description for 548fe16
EperezOk
and
claude
committed
548fe16
View commit details
Copy full SHA for 548fe16
Browse repository at this point
fv: add ERC4626 solvency property (P1)
Show description for 631ad68
EperezOk
and
claude
committed
631ad68
View commit details
Copy full SHA for 631ad68
Browse repository at this point
fv: add ERC4626 round-trip and rounding-gap rules (P2)
Show description for 1c1d1b8
EperezOk
committed
1c1d1b8
View commit details
Copy full SHA for 1c1d1b8
Browse repository at this point
fv: add ERC4626 max/preview boundary rules (P3)
Show description for 9f5875e
EperezOk
committed
9f5875e
View commit details
Copy full SHA for 9f5875e
Browse repository at this point
fv: add ERC4626 conservation and isolation rules
Show description for f0bd86e
EperezOk
committed
f0bd86e
View commit details
Copy full SHA for f0bd86e
Browse repository at this point
fv: shard the ERC4626 config with a complement
Show description for 1b13e6f
EperezOk
committed
1b13e6f
View commit details
Copy full SHA for 1b13e6f
Browse repository at this point
fv: add ERC4626 anti-splitting rules (P4)
Show description for b90b8b0
EperezOk
committed
b90b8b0
View commit details
Copy full SHA for b90b8b0
Browse repository at this point
fv: add ERC4626 rate monotonicity rule (P5)
Show description for 299a4fa
EperezOk
committed
299a4fa
View commit details
Copy full SHA for 299a4fa
Browse repository at this point
fv: add ERC4626 donation-safety rules (P6)
Show description for 7fe7409
EperezOk
committed
7fe7409
View commit details
Copy full SHA for 7fe7409
Browse repository at this point
fv: add ERC4626 donation-sandwich rule (P7)
Show description for 5b1ca1a
EperezOk
committed
5b1ca1a
View commit details
Copy full SHA for 5b1ca1a
Browse repository at this point
fv: record the ERC4626 suite's ledgers
Show description for 03b7af3
EperezOk
committed
03b7af3
View commit details
Copy full SHA for 03b7af3
Browse repository at this point
fv: add the symbolic decimals-offset tier for ERC4626
Show description for e389b1f
EperezOk
and
claude
committed
e389b1f
View commit details
Copy full SHA for e389b1f
Browse repository at this point
fv: rename ERC4626Sandwich to ERC4626Donation and tighten the suite
Show description for 05d6b43
EperezOk
and
claude
committed
05d6b43
View commit details
Copy full SHA for 05d6b43
Browse repository at this point
fv: clarify the offset-pricing note in ERC4626Offset.spec
Show description for d50cf9b
EperezOk
and
claude
committed
d50cf9b
View commit details
Copy full SHA for d50cf9b
Browse repository at this point
fv: link the timeout ledger without line anchors
Show description for 9227618
EperezOk
and
claude
committed
9227618
View commit details
Copy full SHA for 9227618
Browse repository at this point
fv: point the timeout-ledger links at fv-certora.yml
Show description for eea5a38
EperezOk
and
claude
committed
eea5a38
View commit details
Copy full SHA for eea5a38
Browse repository at this point
fv: declare the patched package in the ERC4626 configs
Show description for 600561b
EperezOk
and
claude
committed
600561b
View commit details
Copy full SHA for 600561b
Browse repository at this point
fv: move the ERC4626 timeout notes onto the rules
Show description for f4b085e
EperezOk
and
claude
committed
f4b085e
View commit details
Copy full SHA for f4b085e
Browse repository at this point
fv: prove the sum-of-balances invariant for the offset harness
Show description for f14223e
EperezOk
and
claude
committed
f14223e
View commit details
Copy full SHA for f14223e
Browse repository at this point
You can’t perform that action at this time.
