Introduction — Code Security in Web3

Since its earliest days, the Certora Prover has been a powerful tool for finding bugs and ensuring code security in the smart contracts which make up Web3 applications. Writing specifications using the Certora Verification Language (CVL), our customers and Certora’s own personnel have been able to bring the tremendous power of formal verification to bear on projects large and small throughout the Ethereum space.

Formal Verification and the Certora Prover — A Quick Primer

Most readers in this space will already be comfortable with the basics of Solidity and authoring smart contracts, but formal verification (FV) might be less familiar. More experienced users should feel free to jump to the following section, but for our immediate purposes, it is enough to understand a few concepts.

We can call a program correct if it always does what it should do and never does what it shouldn’t. In our formal verifications of smart contracts, these correct and incorrect program behaviors (broadly called properties) are encoded as specifications using our purpose-built language, CVL. A specification file will usually contain a number of these properties, which we generally refer to as rules. A specification and the relevant smart contracts are then passed to the Certora Prover which uses a number of technologies to return an answer for each of the rules: either a given property holds in all possible cases or the tool returns a set of inputs which led to a violation of that property.

The process for finding these answers can be intensely computationally expensive, so much so that formal verification was long considered to be practically impossible. Even today, solving for certain rules or programs still can be too hard, with the tool timing out before it can return an answer. Nonetheless, through a series of complex steps with a variety of clever optimizations, the Certora Prover can tell us that a property always holds or show us an example where it doesn’t. By default, job runs are sent to the cloud and subsequent results are available from a webpage Rule Report.

Using the Prover from VSCode — More Organized, More Convenient, More Scalable

Formal verification is incredibly powerful, but powerful technologies can be challenging to use, especially at first.

As the Certora Prover has developed and matured, we’ve been able to gather and incorporate feedback from users: what is hard, what is missing, what is annoying, what is great. Today, we are excited to announce the release of our improved VSCode Extension, allowing easier and more convenient access to the impressive capabilities of the Certora Prover.

Let’s go through some of the features we’ve built into the extension and how they can help make your workflow faster and more efficient. At the end, look for links to some additional resources on how to learn about using the Certora Prover and as well as the remarkable basis for formal verification.

Creating Your First Verification Job

The new extension makes it easy to set up verification jobs in one of two ways.

Clicking Configure New Job will take you to a Settings pane so you can immediately select the appropriate files and start customizing your job with the desired options. Previously, the primary way to create and customize a new job was using the CLI (command line interface). While Certora Prover access using the CLI is still available, the VSCode extension provides an elegant and convenient alternative that lets users configure and run new jobs without having to worry about writing flags in the command line or creating scripts to specify the desired options. All of the selected options are saved in a newly created configuration file (stored by default in the `certora/conf` directory of the project).

Clicking Upload Configuration File makes a new job based on the file you upload with all of the appropriate files and options already selected and ready to run. As with a new job, it isn’t necessary to create a script with the right options or even to write scripts at all. All of the configuration is done automatically using the config file.

Sharing Verification Jobs

The easy creation of jobs using configuration files makes collaboration much simpler and faster. Share your job with your colleagues by pushing the corresponding configuration file to your repo. Anyone on your team can then easily pull it to their machine and the job will be ready to go. Make a configuration file publicly available to let others see how you’re setting things up or browse from files others have posted to find setups you can adapt for your own needs. You can even sync the entire `certora/conf` directory, giving your whole team access to the same pool of jobs to work with and avoiding the need to set up jobs of different types multiple times.

Finding and Triggering Jobs

Those who have undertaken even a moderately complex verification project will know how easy it is to find yourself wading through open tabs with the results of different jobs, trying to remember which settings were used where, and thinking you should have been more descriptive in your verification messages. The job list makes it easy to find any of your jobs and see the results along with the settings used for that job.

Running and rerunning jobs is also easy with the VSCode extension, providing quick flexibility in starting runs of different types. Icons in the job list allow you to run all jobs in a project, run a single job, or run just a single rule, all without needing to maintain or edit multiple scripts with different options. Create a duplicate of a job or delete an unneeded job by clicking the icons. Now everything is available in one convenient, accessible place.

Adjusting Settings

It is also now much easier to make changes to an existing job before running it again. The Settings pane lets you see and change all of the relevant details for a given job. Experiment with the original to try a different approach or duplicate the job and adjust its settings to try a few different approaches in parallel. Change compiler versions, link a different file, adjust Prover properties, or add a different verification message, everything can be done easily in one place. And all job configurations are saved and ready to be shared when you have something you’d like others to see.

Job Status and Reports

The extension makes it easy to check the status of your jobs from within VSCode as well. Familiar icons show the status of a rule or job just as you would see using the Prover’s web-based Rule Report. And a single click allows quick access to that Rule Report online, avoiding the need to keep multiple tabs open to access detailed information about the results of running a job.

A New Verification Workflow

We’ve been working hard to make the Certora Prover more capable and easier to use. With the release of this updated extension for VSCode, it is faster and easier than ever to leverage the power of formal verification in your projects.

To install the Certora Prover VSCode extension and learn more about how to use it, follow the instructions found here.

• If you’d like to try the Certora Prover, follow the instructions here to get access and install the tool. Then take a look at the resources here to start learning how to write your own specifications and formally verify your smart contracts.
• If you’re interested in learning more about formal verification and how the Certora Prover pipeline solves these complex problems, watch this video from a recent workshop or read our white paper for a thorough overview.