Smart contracts are designed to carry out financial transactions involving millions of dollars. Bugs in these programs are known to have severe consequences. Naturally, formal verification plays a critical role in this domain. In this blog, we present Certora’s recent efforts towards formally verifying Wasm bytecode.

In this blog, we discuss our efforts to apply mutation testing in the context of automated verification.