Introduction

As the value of assets on the blockchain grows rapidly with several projects taking turns to launch different use cases within the crypto economy, staying ahead of possible loopholes and threats is more imperative than ever.

Bitcoin was invented to replace banks, but the underlying technology, blockchain proved it could replace almost any intermediary. Moving forward, it did not stop there seeing the massive potential that digital money possessed which paper cash never could and that involves the ability to program money. Suddenly, lawyers and contracts could be substituted in financial transactions. This form of digital currency advanced decentralization by enabling the automatic execution of contracts with complete transparency and no human intervention. However, how exactly do smart contracts operate? Is it truly dependable to trust in these systems that lack trust?

In this article, we will explore the extensive questions about the formal verification of smart contracts, discussing its pros, cons, impact on the crypto ecosystem, and more with emphasis on Ethereum.

Brief History of Smart Contracts

Source: CryptoSlate

Nick Szabo, an American computer scientist and cryptographer often speculated to be Satoshi Nakamoto, was the pioneer of smart contracts, first introducing the concept in 1994. Szabo described smart contracts as digital transaction protocols designed to automatically enforce the terms of an agreement. His goal was to enhance electronic transaction methods, such as point-of-sale systems, and expand their capabilities into the digital world.

Szabo envisioned a future where agreements could function like vending machines—automated, reliable, and tamper-proof. Although the technology of his time was not advanced enough to fully realize his vision, Szabo’s ideas laid the foundation for what would later revolutionize the blockchain industry. When Ethereum launched in 2015, it brought smart contracts into practical use, turning Szabo’s theoretical concepts into essential components of decentralized applications.

His vision was for contracts that could manage relationships with precise, automated terms, reducing the need for human intervention and oversight. This approach aimed to create a more secure and efficient way to handle agreements, paving the way for the evolution of smart contracts into powerful tools in the blockchain ecosystem. Szabo’s early insights continue to shape the landscape of digital transactions and smart contract development today.

What is Formal Verification?

Source: Medium

Formal verification is the process of rigorously assessing whether a system, like a smart contract, operates according to a defined set of rules or specifications. In essence, it checks if the system behaves as expected, ensuring that it meets the required conditions and performs the intended functions without errors.

To achieve this, expected behaviors of the system are outlined using formal models, while specification languages are used to define the exact properties the contract must satisfy and we will see more practical scenarios as the article progresses. Formal verification techniques then match the contract’s implementation against its specifications, providing mathematical proof of its correctness. When a contract meets these specifications, it is considered “functionally correct” or “correct by design,” confirming its reliability and security in the blockchain environment.

Types of Formal Specifications for Smart Contracts

Source: Ever Scale

Formal specifications provide a structured way to use mathematical reasoning to verify the accuracy of a program’s execution. These specifications can describe either high-level properties, which focus on the overall behavior, or low-level details of how a contract operates internally. By defining these behaviors mathematically, formal specifications ensure that the contract performs as intended.

High-level specifications

High-level specifications, also known as model-oriented specifications, describe the overall behavior of a smart contract, treating it as a finite state machine (FSM) that transitions between different states through specific operations. Temporal logic is often used to define the formal rules that govern these transitions, detailing how the contract moves between states over time and the conditions it must meet to do so correctly.

These specifications capture two essential properties: safety and liveness. Safety ensures that undesirable events do not occur, such as preventing a sender’s balance from dropping below the amount needed for a transaction. Liveness, conversely, ensures that the contract continues to function and progress, such as maintaining liquidity so that users can withdraw funds when requested. Both properties ensure smart contracts operate securely and reliably, safeguarding user interactions and assets.

Low-level specifications

Low-level specifications, also known as property-oriented specifications, focus on defining the correct behavior of smart contracts by analyzing their internal execution processes. Unlike high-level specifications that model contracts as finite-state machines, low-level specifications view smart contracts as systems of mathematical functions and examine the sequences of function executions, known as traces, that change the contract’s state.

Techniques for Formal Verification of Smart Contracts

Source: Ever Scale

Model Checking

Model checking is a formal verification method that uses algorithms to evaluate whether a smart contract’s model aligns with its specifications. Smart contracts are typically represented as state-transition systems, and their properties are defined using temporal logic. This process involves creating a mathematical model of the contract and expressing its properties through logical formulas, allowing the algorithm to verify if the model meets these specifications.

Theorem Proving

Unlike model checking, theorem proving is a mathematical approach used to establish the correctness of programs, including smart contracts. This method involves converting a contract’s model and specifications into logical formulas to verify their logical equivalence, meaning one statement is true if the other is true. By formulating this relationship as a theorem, an automated theorem prover can validate the correctness of the contract model against its specifications.

In sharp contrast with model checking, which is limited to finite-state systems, theorem proving can analyze infinite-state systems but often requires human guidance to navigate complex logic problems. Consequently, theorem proving tends to be more resource-intensive than the fully automated model-checking process.

Symbolic Execution

Symbolic execution is a powerful analysis method for smart contracts that involves executing functions with symbolic values rather than specific inputs. This formal verification technique allows for reasoning about trace-level properties in a contract’s code by representing execution paths as mathematical formulas, known as path predicates. An SMT solver is then employed to determine if these predicates are satisfactory, meaning an input that meets the conditions exists.

For example, if a contract function reverts when a value is between 5 and 10, symbolic execution can efficiently identify such triggering values by evaluating the condition as X > 5 ∧ X < 10. This method is often more effective than traditional testing, producing fewer false positives and directly generating concrete values that replicate any SMT solver is then employed to determine errors found, thus making it a valuable tool for ensuring smart contract reliability.

What are Smart Contracts?

Source: Tenderly

Smart contracts are automated computer programs that operate on a blockchain, executing actions when specific conditions are met. They can vary from straightforward agreements to highly complex processes and can manage assets valued at millions or even billions of dollars.

While smart contracts have the potential to revolutionize various sectors such as political voting, supply chain management, healthcare, and real estate, this article still maintains its focus on their impact in the cryptocurrency realm. Their design allows multiple parties to collaborate without the risk of manipulation, offering a transparent and secure framework that enhances efficiency and innovation. However, it’s important to recognize that smart contracts also come with vulnerabilities and challenges.

Vulnerabilities with Smart Contact

Security vulnerabilities in smart contract code can lead to catastrophic outcomes, such as the total loss of assets stored within the contract, as demonstrated by recent incidents.

• In 2021, the automated market maker Uranium Finance suffered a theft of $50 million due to a simple typo in its smart contract.
• Also in 2021, Compound Finance inadvertently distributed $80 million in unearned rewards, again because of a single character error.
• A more significant breach occurred in 2022 when $320 million was stolen from the Wormhole Bridge due to a bug in one of its smart contracts.

Given these examples, it is crucial to ensure that smart contracts are coded accurately from the outset. Once deployed, smart contracts are open-source, meaning their code is publicly accessible, making it easy for hackers to exploit any discovered vulnerabilities. Additionally, the immutable nature of smart contracts means that once they are launched, their code typically cannot be altered to patch security flaws, leaving them perpetually at risk if not developed with utmost precision.

How Does Smart Contract Verification Work?

Source: Certik

The process includes:

• Defining the specifications and desired properties of the contract using formal language.
• Translating the contract’s code into a formal representation, such as mathematical models or logical expressions.
• Automated theorem provers or model checkers are employed to confirm the validity of the contract’s specifications and properties.
• Iteratively repeat the verification process to identify and correct errors or deviations from the intended properties.

Key Features of Smart Contracts

Source: Certik

Think of smart contracts as agreements etched in stone once created, they cannot be altered. Operating on a blockchain’s immutable ledger, these contracts automatically enforce terms without the need for intermediaries, which accelerates transactions and lowers costs. This fixed nature enhances security and decentralizes control, significantly reducing the chances of fraud and corruption.

Why Smart Contract Verification is Important

Mathematical reasoning plays a crucial role in ensuring that formally verified smart contracts are free from bugs, vulnerabilities, and unexpected behaviors. This rigorous process boosts trust and confidence in the contract since its properties have been thoroughly validated.

Successful smart contract verification examples highlight its importance in preventing significant financial losses.

Uniswap

For instance, Uniswap, a well-known automated market maker (AMM), underwent formal verification during the development of its V1 smart contract, which identified and corrected rounding errors that could have drained funds.

Balancer

Similarly, Balancer V2, another AMM, benefited from formal verification that discovered an incorrect fee calculation related to flash loans, preventing potential theft.

SafeMoon

SafeMoon V1 had a subtle bug identified through formal verification after deployment. This bug allowed the owner to renounce ownership and regain it under certain conditions, a detail that most manual audits missed due to its complexity. Formal verification’s ability to analyze specific combinations of variable values makes it an effective tool for catching issues that human auditors might overlook.

How Formal Verification and Manual Auditing Work Together

Formal verification offers a systematic and automated method for checking a smart contract’s logic and behavior against its intended properties. This approach simplifies identifying and correcting potential errors or bugs, particularly complex issues that manual inspections might overlook.

On the other hand, manual auditing involves an expert’s thorough review of the contract’s code, design, and deployment. The auditor leverages their experience to pinpoint security risks and assess the overall security posture of the contract. They can also validate the correctness of the formal verification process and identify issues that automated tools might miss. Combining formal verification with manual auditing creates a comprehensive security evaluation, increasing the likelihood of uncovering and resolving vulnerabilities, and establishing a robust defense strategy that harnesses the strengths of both human expertise and automated analysis.

Pros and Cons of Smart Contracts

Source: Blockonomi

Smart contracts aren’t perfect, but their advantages significantly outweigh the drawbacks. They simplify complex transactions, saving time and money while promoting transparency and reducing disputes. Since they operate on code, they minimize human errors. Their security is robust, thanks to cryptographic protections. However, smart contracts can be inflexible and struggle to adapt to unexpected situations. Additionally, setting them up requires specialized coding skills, which can be a barrier for some. Despite these challenges, smart contracts are transforming industries.

Pros of Smart Contracts

• Improve efficiency by automating tasks, saving time and money.
• Increase transparency by giving all parties access to the same information, reducing disputes.
• Reduce mistakes by relying on code, which eliminates human error.
• Strengthen security with cryptographic protections, making tampering difficult.

Cons of Smart Contracts

• Lack of flexibility to adjust to unforeseen situations due to their rigid nature.
• Require specialized coding knowledge, limiting widespread adoption.

Formal Verification Tools for Ethereum Smart Contracts

Source: Calibraint

Specification languages for creating formal specifications

• Act: Act enables users to define storage updates, pre and post-conditions, and contract invariants. Its tool suite includes proof backends that can validate various properties using Coq, SMT solvers, or hevm.

GitHub

Documentation

• Scribble: Scribble converts code annotations written in its specification language into specific assertions that verify the specifications.

Documentation

• Dafny: Dafny is a programming language designed for verification, using high-level annotations to help reason about and confirm the correctness of code.

GitHub

Program verifiers for checking the correctness

• Certora Prover: Certora Prover is an automated formal verification tool that checks the correctness of smart contract codes. Specifications are created using the Certora Verification Language (CVL), and it detects property violations through a mix of static analysis and constraint-solving techniques.

Website

Documentation

• Solidity SMTChecker: Solidity’s SMTChecker is an integrated model checker that uses Satisfiability Modulo Theories (SMT) and Horn solving. It verifies whether a contract’s source code aligns with specifications during compilation and checks for safety property violations.

GitHub

• Solc-verify: Solc-verify is an enhanced version of the Solidity compiler that enables automated formal verification of Solidity code through annotations and modular program verification.

GitHub

• KEVM: KEVM formally represents the Ethereum Virtual Machine (EVM) created using the K framework. It is executable and can verify specific property-related claims through reachability logic.

GitHub

Documentation

Logical frameworks for theorem proving

• Isabelle: Isabelle/HOL is a proof assistant that helps users express mathematical formulas in a formal language and provides tools for proving them. Its primary use is formalizing mathematical proofs, especially for verifying the correctness of computer hardware and software and the properties of programming languages and protocols.

GitHub

Documentation

• Coq - Coq is an interactive theorem prover that allows you to define programs with theorems and create machine-checked proofs of their correctness through an interactive process.

GitHub

Documentation

Symbolic execution-based tools for detecting vulnerable patterns in smart contracts

• Manticore - A tool that analyzes EVM bytecode using symbolic execution.

GitHub

Documentation

• Hevm - hevm is a symbolic execution engine that checks the equivalence of EVM bytecode.

GitHub

• Mythril - A symbolic execution tool used to find vulnerabilities in Ethereum smart contracts.

GitHub

Documentation

Conclusion

To safeguard smart contracts, combining formal verification with manual auditing is crucial for a comprehensive assessment of their security. Though formal verification can be resource-heavy, it is a valuable investment for contracts involving high stakes or significant risk. Smart contracts are more than a trendy concept; they are transforming global business operations, and while they come with challenges, their unparalleled ability to increase efficiency, minimize errors, and bolster security cannot be ignored. Smart contracts hold tremendous potential to simplify processes and foster trust in digital transactions. To this end, organizations that adopt this technology today will be poised to thrive in a future that prioritizes transparency and dependability.