Formal verification is a method of mathematically proving that a computer program functions as intended. It involves expressing the program's properties and expected behavior as mathematical formulas, and then using automated tools to check that these formulas hold true. This process helps ensure that the program meets its desired specifications.

Formal verification techniques can be applied to many systems, including:

• Computer hardware design: Ensuring that integrated circuits and digital systems meet their desired property specifications and behave correctly.

• Software engineering: Verifying the correctness and reliability of software systems, especially in mission-critical applications such as aviation, medical devices, and financial systems.

• Cybersecurity: Evaluating the security of cryptographic algorithms and protocols, and identifying vulnerabilities in security-sensitive systems.

• Artificial intelligence and machine learning: Verifying the properties and behavior of AI and ML models, ensuring that they operate as intended and make accurate predictions.

• Automated theorem proving: Verifying mathematical theorems and proving mathematical conjectures, which has applications in fields such as mathematics, physics, and computer science.

• Blockchain and smart contracts: Ensuring the correctness, security, and reliability of blockchain systems and smart contracts.

Formal Verification of Smart Contracts

Formal verification of smart contracts works by representing the logic and desired behavior of smart contracts as mathematical statements. Then, auditors use automated tools to check if these statements are correct.

The process involves:

1. Defining the specifications and desired properties of a contract into formal language.
2. Translating the code of the contract into a formal representation, such as mathematical models or logic.
3. Using automated theorem provers or model checkers to validate that the specifications and properties of the contract hold true.
4. Repeating the verification process to find and fix any errors or deviations from the desired properties.

Sometimes the automated theorem provers or model checkers cannot prove or disprove that a property holds true. In this case, the specifications and desired properties may need to be refined and the formal methods repeated.

The specifications and desired properties can be refined by applying more specifications to smaller pieces of code or making the specifications more detailed. This can make it easier for the theorem provers and model checkers to validate that specifications and properties hold true.

Formal verification can be applied to one contract or to multiple contracts at a time. Web3 projects often use multiple contracts, and it is important to make sure that the contracts work together and implement the desired project functionality correctly.

This use of mathematical reasoning helps to ensure that formally verified smart contracts are free from bugs, vulnerabilities, and other unintended behavior. It also helps to increase trust and confidence in the contract, as its properties have been rigorously proven to be correct.

Translating code into a formal representation

Code Snippet 1 shows a simplified program that implements a token transfer function. There are two users that each have a balance of tokens (balance and balance2). The function transferFromUser1 transfers tokens from User 1 to User 2. The program has an invariant that the total supply of tokens always equals the sum of the balances.

uint balance1;
uint balance2;
uint totalSupply;

// Transfer money from User 1 to User 2.
function transferFromUser1(uint amount) {
    balance1 = balance1 - amount;
    balance2 = balance2 + amount;
}

Code Snippet 1: A simple program illustrating a transfer

We represent the invariant as a mathematical formula. We number formulas to keep track of them. Because formulas are mathematical, = means “equals”, not assignment, in them:

Formula 1: totalSupply =  balance1 + balance2     // sum of balances

Code Snippet 2 shows how we can add logical formulas representing what is true at each point in the function. For simplicity, we ignore the possibility of integer overflow. Handling that would make the formulas much longer.

function transferFromUser1(uint amount) {

  // Formula 1: totalSupply = balance1 + balance2

  balance1 = balance1 - amount;

  // old(balance1) represents the value of balance1 when entering the function.
  // Formula 2: totalSupply = old(balance1) + balance2
  // Formula 3: balance1 = old(balance1) - amount // implied by the assignment
  // Formula 4: Formula 2 ^ Formula 3

  balance2 = balance2 + amount;

  // old(balance2) represents the value of balance2 when entering the function.
  // Substitute old(balance2) into Formula 4, replacing balance2.
  // Formula 5: (totalSupply = old(balance1) + old(balance2)) ^
  //            (balance1 = old(balance1) - amount)
  // Formula 6: balance2 = old(balance2) + amount   // implied by the assignment
  // Formula 7: Formula 5 ^ Formal 6.
  // Formula 7 expands to:
  //            (totalSupply = old(balance1) + old(balance2)) ^
  //            (balance1 = old(balance1) - amount) ^
  //            (balance2 = old(balance2) + amount)
}

Code Snippet 2: Function with logical formulas representing the meaning of the code.

If we want to check that transferFromUser1 maintains the program invariant, we can check that Formula 7 (at the end of the function) implies the invariant (Formula 1). Here is the proof, using high-school algebra simplification rules.

Assume Formula 7 is true 
Solve for old(balance1) and old(balance2) using the last 2 clauses of Formula 7:
  old(balance1) = balance1 + amount
  old(balance2) = balance2 - amount
Substitute that into the first clause of Formula 7:
  totalSupply = (balance1 + amount) + (balance2 - amount)
Cancel addition and subtraction of amount:
   totalSupply = balance1 + balance2

How Formal Verification and Manual Auditing Work Together

Formal verification and manual auditing complement each other in ensuring the security of smart contracts.

Formal verification provides a systematic and automated way to check the contract's logic and behavior against its desired properties. This makes it easier to identify and fix any potential errors or bugs. It is especially useful for finding complex and subtle issues that may be difficult to detect through manual inspection.

When dealing with complex or multiple contracts, it can become difficult for a human to reason about all the possible combinations and cases that need to be checked. Machines, however, are well-suited to this task.

Manual auditing provides a human expert review of the contract's code, design, and deployment. The auditor can use their experience and expertise to identify potential security risks and evaluate the contract's overall security posture. They can also verify that the formal verification process was performed correctly, and check for issues that may not be detectable with automated tools. Their expert insight helps ensure that the specifications and desired properties used in formal verification are indeed the right ones.

Combining formal verification and manual auditing provides a comprehensive and thorough evaluation of a smart contract's security. This increases the chances of finding and fixing any vulnerabilities. The result is a defense-in-depth approach to security that leverages the unique capabilities of both humans and machines.

Conclusion

This article serves as an introduction to formal verification and how it can be applied to increase the security of smart contracts and decentralized applications. Stay tuned for a forthcoming technical deep dive into the formal verification of ERC-20 tokens.