Smartcontracts need to do as designed and perform without any errors. Especially when they carry high value transactions. For this purpose, the native smartcontract language in Tezos, offers something that is called "formal verification". It enables the developer to "formally verify" whether or not the written contract performs as it should, before it is deployed on the blockchain. This methodology is commonly used in mission-critical environments such as the aerospace, nuclear, and semiconductor industries.
This quality is something that has earned interest from several STO (Security Token Offering) issuing platforms that have chosen Tezos as blockchain of preferred choice.
Formal verification is a valuable quality to offer on a smartcontract platform like Tezos, but to formally verify your code, you still need to know how to do so: this feature requires specialized knowledge.
The University da Beira Interior in Portugal has published a paper that introduces WhylSon, which is one of the results of the FRESCO project, which is supported by the Tezos Foundation. WhylSon is a tool for automated formal verification of smartcontracts written in Michelson, and allows integration with the Why3 framework. (Why3 is an existing platform for deductive program verification.)
For now this tool is designed for smartcontracts written in Michelson, but Tezos has more languages available for developers that want to deploy smartcontracts on Tezos. "So an interesting long-term line of work to explore is to connect WhylSon with certifying-certified compilation techniques and platforms. For instance, we should evaluate how the integration of WhylSon with, e.g., the Archetype platform, that also makes use of Why3, can benefit the automatic proof of Michelson smart contracts."
The University da Beira Interior in Portugal has published a second paper that introduces another tool: "Tezla". This tool aims for a simplified static analysis of smartcontracts. "To facilitate the usage of such tools to verify Michelson smart contracts, we present Tezla, a store based intermediate representation language for Michelson, and its respective tooling. We provide an automated decompiler of Michelson smart contracts to Tezla. The decompiler preserves the semantics, flow and resource usage of the original smart contract, so that properties like gas consumption can be faithfully verified at the Tezla representation level. "
Two great tools to simplify safer smartcontract development. The Tezos ecosystem keeps on delivering more innovative solutions.
------------------
New to Tezos? Read this full introduction to Tezos.
