SMTChecker: (almost) practical superpower

A tool that performs formal verification of your contract: you define a specification and SMTChecker formally proves that the contract conforms to the spec.

Would you bet your firstborn that the contract you just deployed doesn’t have critical vulnerabilities? If you’re like me, the answer is a resounding β€˜no’. I’ve seen enough hacks in traditional software engineering to know that you can never be 100% sure. That is scary, but a combination of different techniques can get us pretty close to the desired level of confidence. SMTChecker is one of them.