Stainless
Verification framework for a subset of the Scala programming language. See
Quick start
Download the latest stainless-dotty-standalone
release for your platform.
Unzip the archive, and run Stainless through the stainless.sh
(or stainless.bat
) script.
Stainless expects a list of space-separated Scala files to verify.
To check if everything works, you may create a file named HelloStainless.scala
next to the stainless.sh
script with the following content:
import stainless.collection._
object HelloStainless {
def myTail(xs: List[BigInt]): BigInt = {
require(xs.nonEmpty)
xs match {
case Cons(h, _) => h
// Match provably exhaustive
}
}
}
and run stainless.sh HelloStainless.scala
.
If all goes well, Stainless should report something along the lines:
[ Info ] βββββββββββββββββββββ
[ Info ] βββ‘ stainless summary ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
[ Info ] β βββββββββββββββββββββ β
[ Info ] β HelloStainless.scala:6:5: myTail body assertion: match exhaustiveness nativez3 0,0 β
[ Info ] ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ’
[ Info ] β total: 1 valid: 1 (0 from cache) invalid: 0 unknown: 0 time: 0,0 β
[ Info ] ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
[ Info ] Shutting down executor service.
This archive of Stainless only requires JDK17. In particular, it needs neither a Scala compiler nor SBT. It is shipped with Z3 4.8.14 and Princess.
SBT Stainless plugin
Alternatively, one may integrate Stainless with SBT. The supported Scala versions are 3.2.0
and 2.13.6
To do so, download sbt-stainless, and move it to the directory of the project.
Assuming the project's structure is:
MyProject
βββ build.sbt
βββ project
β βββ build.properties
βββ sbt-stainless.zip
βββ src/
Unzipping sbt-stainless.zip
should yield the following:
MyProject
βββ build.sbt
βββ project
β βββ build.properties
β βββ lib <--------
β βββ sbt-stainless.jar <--------
βββ sbt-stainless.zip
βββ src/
βββ stainless/ <--------
That is, it should create a stainless/
directory and a lib/
directory with project/
.
If, instead, the unzipping process creates a sbt-stainless/
directory containing the lib/project/
and stainless/
directories,
these should be moved according to the above structure.
Finally, the plugin must be explicitly enabled for projects in build.sbt
desiring Stainless with .enablePlugins(StainlessPlugin)
.
For instance:
ThisBuild / version := "0.1.0"
ThisBuild / scalaVersion := "3.2.0"
lazy val myTestProject = (project in file("."))
.enablePlugins(StainlessPlugin) // <--------
.settings(
name := "Test"
)
Verification occurs with the usual compile
command.
Note that this method only ships the Princess SMT solver. Z3 and CVC4 can still be used if their executable can be found in the $PATH
.
Build and Use
To start quickly, install a JVM and use a recent release. 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.
Further Documentation and Learning Materials
To get started, see videos:
- ASPLOS'22 tutorial
- FMCAD'21 tutorial
- Formal Verification Course: Getting Started, Tutorial 1 Tutorial 2 Tutorial 3 Tutorial 4, Assertions, Unfolding, Dispenser Example
- Keynote at Lambda Days'20
- Keynote at ScalaDays'17 Copenhagen
or see local documentation chapters, such as:
There is also a Stainless EPFL Page.
License
Stainless is released under the Apache 2.0 license. See the LICENSE file for more information.
Inox
Relation toStainless 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.