Integration Checklist

[baolean]

• Using setUp() result to initialize contract(s) state
• Symbolically execute functions starting with prove
• Detect failed assets in solc >= 0.8
• Decode function names in counterexamples
• Detect failed asserts in solc < 0.8
  
• Detect forge's asserts
  
• Set block.timestamp and block.number values in geth based on the attack counterexample
• Make solver and its timeout configurable
• Fix view/pure functions analysis
• [WIP] Detect reverts w/ specific error messages (Done for "Overflow")
• [WIP] Add "symbolic storage" mode
• Fix loop detection
• Consider using ethers instead of geth for validation
• Support Foundry and hevm cheatcodes, e.g., warp
• Implement CREATE and constructor support
• Investigate false positives w/o concrete validation