A collection of useful Vyper contracts developed with formal methods
WARNING: These contracts are not audited and formal verification is WIP. Take care when you use them for production.
The /contracts directory contains vyper contracts we use in formal verification (/k directory) and unit testing ( /tests directory).
The /k directory contains files to do formal verification with K Framework.
The /tests directory contains unit tests.
See roadmap.
This project is based on K Framework and Runtime Verification's works. See their resources for the details of KEVM and background knowledge.
FVyper is supported by KEVM and Vyper teams. We’d like to express thanks to them and their great work.