Smart-proven contracts

Smart-proven contracts Build • Valentin Macheret • 07/01/25 • 5 min read

In the decentralized-storage ecosystem, a specific type of program is used for storage access: smart contracts. They are used for anything to read or write over a public decentralized database (aka blockchain). They are deployed over multiple nodes of a network and will be executed when needed (for record, trade, election, any kind of process...). Smart contracts are intended to be in charge of the integrity of the data and transaction, that makes them particularly critical, like a 'real contract'.

New kinds of tools are slowly making their way to ensure smart-contract reliability. Let's see how.

Criticality of smart contracts

One fundamental leitmotiv of a blockchain is trustlessness: you don't need to trust someone in particular to interact with (indeed, the trust is shared because decisions are decentralized, data are immutable, there is voting by consensus...).

However, smart contracts are still basic programs. They can be buggy or malicious. They easily broke this trustless principle. One way to be sure that a smart contract is really doing well could be resolved by introducing a lot of tests, but corner cases are hard to mitigate.

Classical testing limits

By writing unit/behaviour testing and assertion checks you will need a huge amount of tests (and time) to guarantee that by calling function 'A' with argument 'x', you will get 'y' and avoid any side effects into the rest of your program. Furthermore, assertions and tests are runtime-based , so you need to simulate a small blockchain and i/o.

A solution to this labour could be to write our program as a way to be sure-by-design regarding its behaviour (integrity & reliability). This assertion is equivalent to building a mathematical proof that our program satisfies a property at a given time. Building such a proof is equivalent to make the formal verification of our program.

Formal verification of programs

We do formal verification by checking -in a determinist way- that the program behaviour satisfies some requirements, basically verify that it does what we want . However, these properties are described using a formal modeling, a kind of mathematical description of computation, axioms and states. Model-checking and theorem-proving are the two main prominent methods in that field.

This is very different from classic testing or assertion methods! Indeed the verification is done upstream while unit test/assert is done at runtime.

Formal verification allows us to prove that some behaviours will never occur because it was written that way.

Formal methods are still in research and development for decades by logicians and computer scientists. Because potential pay-offs of formal verification are high, there is a big shift between true-formal partisans and pragmatic people, who favor more direct and inquiry-relative ways to test and evaluate programs.

Smart contracts are good candidates to reunify both sides. They are small, very domain specific, public and they must be rock-solid on what they are supposed to do: critical operations on sensitive stuff. They are immutable, so any mistake or vulnerability can lead to a disaster.

Nevertheless, verifying a program from scratch is a huge undertaking that requires time and specialists skilled into formal methods. We need tooling to bring this valuable paradigm into more common programming.

Here an overview of the current state and efforts to understand the usage of formal verification in smart contracts.

Verify existing languages

Smart contracts are actually written using domain specific programming languages. There are relatively few programming languages that are well-suited to work with, and some of the available languages can be difficult to learn or use.

We can enumerate: Clarity for Bitcoin, Solidity or the less-buggy Vyper for Ethereum-based blockchains, Liquidity or any Michelson transcript tool for Tezos (because nobody will force you to write anything in Michelson).

There are efforts to bring formal method verification into contracts, one way is to verify the language it-self. It means: avoid any by-design mistake of a language (overflow, underflow, mistyping) that can be error prone.

On Ethereum VM

Working on Ethereum-based smart contracts (mostly) imply Solidity : it is a powerful and flexible language that is widely adopted. However, it can be difficult to write secure and reliable programs, as it is easy to make mistakes that could compromise the security or functionality of a contract. This is a well-known issue.

Indeed, Solidity comes with its inherent problems:

Too permissive / on the very top of the Ethereum Virtual Machine (EVM)

Procedural-coding is encouraged, not good to apply constraints over property

Language compiler is changing too quickly for verification tools to keep up

The only way to know the meaning of a Solidity contract is to compile it into bytecodes

How to ensure that the bytecode behaviour is the same from the high level language?

Efforts made over the Ethereum blockchain are present as well as academic research engaged to modelize the EVM. However, concrete and production-ready tooling are absent. Indeed, it is highly non trivial to evaluate a language's robustness from a language that was not designed for. It requires to be translated into a provable language. However, original semantics can be lost in the process...

There is, like this Ethereum initiative to provide an EVM Isabelle implementation , or to formally verify the Vyper language . It leds to a fine bug tracking which highlight this kind of funny issues like this one or this one , where compiler initialization or call incoherences were found.

Since the announcement in 2016 and some projects or proof-of-concept articles , nothing more has been done over EVM. The consequence of a lack of profile working on these subjects.

Current efforts are focus on security analysis tools like Sourcify or Mythril ; which uses symbolic execution to analyze Solidity codebase and generated bytecode to identify potential vulnerabilities.

A common workaround to track contract vulnerabilities remains bug bounty. There are many bounty platforms like Hacken or Immnuefi...

On Tezos

On the other hand Tezos is leading formal verification applied to smart contracts by proposing proof-tooling to interact with its blockchain. They intend to fully certify…