✨ I'm participating in Optimimsm's RPGF Round 3. Check out my submission to support my work

SMTChecker, Remix & Dapptools

Using SMTChecker formal verification module in Solidity compiler with Remix & Dapptools

The SMTChecker is a formal verification module inside the Solidity compiler. Historically it has been complicated to run the SMTChecker on your own contracts, since you had to compile the compiler with an SMT/Horn solver, usually z3. We have been working on different solutions to this, and nowadays it is quite easy to run it.