We look at formal verification & symbolic execution with two Trail of Bits Web3 security team members. Additionally, we review the value these techniques bring and compare them to other tools.

What is Formal Verification? What is Symbolic Execution?

Troy Interview: https://www.youtube.com/watch?v=H52U4ibkf5Q Josselin Interview: https://www.youtube.com/watch?v=3pWYvtx_sjA

✍️ Article: https://medium.com/@patrickalphac/formal-verification-symbolic-execution-38e0ac9072eb 🗻 Code Examples: https://github.com/PatrickAlphaC/denver-security/tree/main 🟩 Comparing Symbolic Execution tools: https://hackmd.io/@SaferMaker/EVM-Sym-Exec 📚 Invariant vs Fuzz: https://ethereum.stackexchange.com/questions/144691/whats-the-difference-between-invariant-and-fuzz-testing 🛠️ Foundry Invariant: https://book.getfoundry.sh/forge/invariant-testing 🦔 Echidna: https://github.com/crytic/echidna