Making sure that smart contracts are secure and bug-free has never been more critical. Unfortunately, it remains a difficult task. While there are helpful tools for automatic testing and formal verification, ensuring the correctness of smart contracts continues to be a time-intensive and challenging task. To make things worse, each tool often has a steep learning curve, and it is often uncertain whether it's even right for the job.

That is why we've developed Scribble: a verification language and runtime verification tool. While initially created for automatic property testing during audits, we've decided to share this project with the community!



What is Scribble?

When we're talking about Scribble, we're talking about two things.

First, Scribble is a specification language for writing properties.
Second, Scribble is a runtime verification tool using the Scribble specification language.

NOTE: Scribble doesn’t perform any verification by itself. It does enable other tools to test and check properties.



Scribble is a language
Scribble defines a domain-specific language for writing properties about smart contracts. We've built the language on top of the solidity syntax, to make it easy to learn. This specification language allows you to annotate a solidity smart contract with properties.

NOTE: A property is a logical statement that you expect to be true, e.g. "All cars are red". In solidity, you'll often have properties like: "Only the owner can make a change to X". Or "Function sendToken(), should not change this contract's ether balance".

You can use several annotation types for different kinds of properties. For example, invariants or post-conditions.

This is an example of a Scribble annotation:

As you can see, the annotations take the form of an inline comment placed above a function definition. We've added a so-called if_succeeds clause, which checks whether a condition holds after the function is executed. In this case, we check that the result of the function is always non-zero.

Read Scribble Documentation

We've based the Scribble language on proven concepts such as post-conditions, invariants and temporal logic. But we also look at how we can introduce novel ideas to suit the domain-specific problems of smart contracts better.



Scribble is a tool
Scribble can take a contract annotated with properties, and compile it into a new contract. In this new contract, Scribble will have added Solidity code that raises an assertion whenever a property is violated. We call this process instrumentation.

Adding executable code that checks properties is called runtime verification, and makes it easy to work with existing tools without many adaptions. This is the case because most tools will already interpret solidity code and be able to search for property violations right away!

Because you can use existing automatic testing techniques (such as our fuzzer Harvey), you'll be able to start testing after writing just a single property. We believe that this is a significant benefit; You benefit from automatic testing right away, instead of having to spend a lot of time upfront to gain a critical mass of annotations. Something which is usually necessary with traditional verification approaches.

You can get started testing and analysing a contract quickly, and even decide later on to put in the additional effort to verify a smart contract completely!



Goals

Audit

We're using Scribble during audits to formulate properties. Using automatic analysis techniques such as fuzzing and symbolic execution, we'll automatically test and find violations for these properties.

Contact us to learn more about fuzzing and property-based testing during audits

Standard

Scribble aims to work with different tools and techniques; we don't just want to enable property-based testing, but also easy formal verification. The benefit of using a single universal specification language is that you only put in the effort of writing properties once, but reap the benefit of using multiple tools.

Adoption

With Scribble we are hoping to lower the barrier or entry for automatic testing and formal verification. We also want to reduce the time investment needed to develop correct and secure smart contracts, resulting in a safer ecosystem.



Where can you get it?

We've wholly open-sourced Scribble, and it's available now at github.com/consensys/scribble.

NOTE: This is a beta-release, aspects of the language will change, and you might encounter some bugs.

You can easily install Scribble with npm:

Install Scribble