Stainless

Verification framework for a subset of the Scala programming language. Supports contract-driven verification as well as termination checking of higher-order functional programs with local imperative features (see Pure Scala and Imperative for more details about the supported fragment).

• Stainless Website at EPFL: https://stainless.epfl.ch
• EPFL-LARA Website: https://lara.epfl.ch/w/

Documentation

To get started, see videos:

• Tutorials from EPFL Course: Getting Started, Tutorial 1 Tutorial 2 Tutorial 3 Tutorial 4, Assertions, Unfolding, Dispenser Example
• Viktor's keynote at Lambda Days 2020
• Viktor's keynote at ScalaDays 2017 Copenhagen

Tutorials such as one from FMCAD 2021, from ASPLOS 2022 or local documentation chapters, such as:

• Documentation
• Introduction to Stainless
• Installation
• Getting Started
• Command-line Options
• Tutorial
• Stainless EPFL Page

Build and Use

To build the project, run sbt universal:stage. If all goes well, scripts are generated for Scala 3 and Scala 2 versions of the front end:

• frontends/scalac/target/universal/stage/bin/stainless-scalac
• frontends/dotty/target/universal/stage/bin/stainless-dotty

Use one of these scripts as you would use scalac to compile Scala files. The default behavior of Stainless is to formally verify files, instead of generating JVM class files. See frontends/benchmarks/verification/valid/ and related directories for some benchmarks and bolts repository for a larger collection. More information is available in the documentation links.

License

Stainless is released under the Apache 2.0 license. See the LICENSE file for more information.

Relation to Inox

Stainless relies on Inox to solve the various queries stemming from program verification. Inox supports model-complete queries in a feature-rich fragment that lets Stainless focus on program transformations and soundness of both contract and termination checking and uses its own reasoning steps, as well as invocations to solvers (theorem provers) z3, CVC4, and Princess.