Stainless (Documentation, GitHub)

Stainless is a tool for verifying Scala programs. Stainless is developed by LARA at EPFL's School of Computer and Communication Sciences. Stainless can verify that your program is correct for all inputs, it can report inputs for which your program fails when they exist, and it can prove that functions do not loop. Using Stainless before running or deploying the software can eliminate crashes, logical errors, security flaws, and other defects.

Main Links

Why Stainless

Stainless is a way to use Scala to develop highly reliable applications, with errors caught early during the development process. Thanks to its use of formal proofs, Stainless can establish safety and termination properties using symbolic reasoning, covering infinitely many inputs in a single run of verification.

One can compare Stainless to proof assistants such as Isabelle/HOL, Coq, or ACL2 in terms of the complexity of some of the program properties it can prove, though it was originally conceived more as a program verifier, such as Dafny. Stainless can be more automated when finding proofs of programs compared to proof assistants, and can also report counter-examples for invalid properties in many non-trivial cases, see counterexamples for bugs in benchmarks such as ConcRope.scala, ListOperations.scala, Mean.scala, PropositionalLogic.scala, AssociativityProperties.scala, InsertionSort.scala, more example reports, or check some of our regression tests. On the other hand, proof assistants are much better at formalizing mathematics than Stainless, especially when it comes to libraries of formalized knowledge.

What Stainless Verifies

Stainless supports verifying:

Stainless ensures that the input program belongs to a subset of Scala. This subset syntactically prevents:

The choice of the subset of Scala along with the checks for runtime errors rules out most known sources of errors in Scala programs. An exception are resource exhaustion errors (but see resource bound analysis in Leon documentation below).

Stainless correctly models integral types such as Int with an appropriate level of bits and takes overflow into account (for unbounded integers, use BigInt).

Stainless performs non-trivial termination checks for its functions and supports specifying decreasing measure functions.

Example Application: Verification of Smart Contracts and Clients

As an example application, we can use Stainless in automated verification of smart contracts. We have created the following fork of Stainless:

https://github.com/epfl-lara/smart

which shows how to:

For example, we have modeled and verified a voting smart contract developed by SwissBorg using Scala and Stainless (check the corresponding benchmark).

For more information, check the README.md, as well as the online documentation including the page on smart contracts in Stainless.

Our verification efforts may prove useful in the future for companies such as AXONI as well. A this stage, our open source implementation of generator for Solidity is a proof of concept, which helps understand the verification challenges as well as differences and similarities of Solidity and Scala programming models.

Beyond verifying individual smart contracts, we are excited about the potential of Stainless to establish properties of clients and wallets for blockchain networks, such as the Mantis client written in Scala as well as Bitcoin-S.

Finally, we are also interested in new programming models for smart contracts and understanding how they can further increase the reliability and efficiency of decentralized systems.

This direction of work with Stainless is inspired by discussions within the EPFL Center for Digital Trust of which our research group is a member.

Stainless is the result of work of many contributors, see the main Stainless repository. Smart contract support is in particular due to the work of Jad Hamza and Romain Jufer. For more information about Stainless for blockchain technologies, please contact Jad and Viktor.

Inox

Stainless derives its verification power from the Inox constraint solver for purely functional recursive constraints:

Inox makes use of SMT solvers Z3, CVC4, and Princess, and adds support for recursion, higher-order functions, its own support for quantifiers, as well as a form of dependent types.

Leon

Stainless and Inox grew out of a verification component of the Leon system (Leon at GitHub, documentation) Stainless supports more Scala features than Leon and can be much more effective for verification. Leon has been developed as a more experimental system and in addition to verification, supports program synthesis, program repair, C-code generation, as well as programming by example. Leon also has web interface called Leon Web, whose source code is available. We also occasionally run it as a limitted-bandwidth service.


2019-05-10. This page is simple and this is its end.