diff --git a/README.md b/README.md index da1396f..0baedab 100644 --- a/README.md +++ b/README.md @@ -61,6 +61,14 @@ describing techniques for which I could not find the actual tool. * [Harvey](https://consensys.net/diligence/blog/2019/01/fuzzing-smart-contracts-using-multiple-transactions/): A fuzzer for Ethereum smart contracts. * [hevm](https://github.com/dapphub/dapptools/tree/master/src/hevm): hevm is many things as you will see below, including a fuzzer. The fuzzer can also be used to try to break invariants. - Article: [Symbolic Execution With ds-test](https://fv.ethereum.org/2020/12/11/symbolic-execution-with-ds-test/), David Terry. + +#### Economics / Game Theory + +* [Clockwork Finance Framework](https://github.com/defi-formal/cff/): A general purpose formal verification framework and mechanized proof system for reasoning about economic security properties of composed DeFi contracts, using K framework's symbolic execution engine and model checker. + - Paper: [Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts](https://arxiv.org/pdf/2109.04347.pdf) + - Talk: [Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts - SBC22](https://www.youtube.com/watch?v=n52xBSk2TSs) + - Slides: [Clockwork Finance](https://www.cs.cornell.edu/~babel/slides/cff_sbc_pdf.pdf) + #### EVM Bytecode