At DeepReason, we build automated formal verification. Understanding this requires first understanding

  1. formal verification and then what it means to
  2. automate it

We at DeepReason believe that popularizing the use of effective formal verification technology holds the key to a more secure, sustainable, and exciting future for web3. We envision it providing the confidence for faster audits and faster innovation.

🧠 What is formal verification (FV)?

Formal verification is the technique of mathematically modeling code, and then making mathematically-guaranteed claims about that code. It makes rigorous any claims an auditor might have about the function of a software program. In the context of smart contracts, it allows you to create rigorous proofs of security for a smart contract.

Formal verification has only recently become practical and effective in real-world applications. Formal verification of a program becomes slower when the program being verified is more complex. At DeepReason, we are working on advancing the speed of this technology.

🤔 How do you mathematically model a program?

You can mathematically model a computer program using the idea of symbolic execution. Normally, a computer program takes in a concrete set of inputs and spits out a concrete set of outputs:

$$ \{2,9\}\xrightarrow{\text{Program}} \{85, 18\} $$

What is this program even doing? It is hard to tell just by looking at this. Well, when using symbolic execution, a program runs on a set of symbolic variables that represent the inputs. The outputs, and every intermediate calculation, are then all mathematical expressions based on the input variables:

$$ \{x,y\}\xrightarrow{\text{Program}} \{x^2+y^2, 2y\} $$

As you can see, running symbolic programs immediately gives more insight into what is happening. Any claim about the software program can then be expressed as a mathematical claim based on these variables.

At this point, a human or sufficiently powerful automated reasoning engine can prove or disprove claims about the program. In the example above, it could prove that the first output is always non-negative and the second output is always even.

🚀 DeepReason: Automating formal verification

Although formal verification is a powerful tool, it needs to be applied in the right ways to effectively solve your web3 company’s security challenges. Currently, after the mathematical modeling, the current state of formal verification involves manually writing the specs/proofs.

😳 Issues with manual Formal Verification

  1. Difficult to set up. Using FV often requires expert knowledge about logical systems and sometimes knowledge of a specific language used to write FV logic.
  2. You risk incorrectly writing your specifications. There have been many high-profile projects that have been exploited despite employing FV in some manner. All of them came down to the human error of writing the wrong or incomplete set of security specifications.

<aside> ⚠️ Few teams should rely on writing their own formally verified specifications. Even expert manual auditors have made mistakes in the past.

</aside>