Verification framework for a subset of the Scala programming language. See the tutorial.
This archive of Stainless depends on an experimental version of Inox with
prototype support for Horn solvers. The examples from the HCVS 2024 paper can be
found in the inductiveExamples/ directory.
You will need sbt to run these examples. General installation instructions are
in the following sections.
After booting up sbt, the examples can be run with the following pair of commands:
> project stainless-dotty
> run ../../inductiveExamples/fibonacci.scala --solvers=horn-z3 --vc-cache=false(The ../../ is required as the working directory is ./frontends/dotty for
the Scala 3 compiler frontend.)
The solvers can be changed to horn-eld for Eldarica, or smt-z3, smt-cvc5,
and princess for the usual supported backends. For the McCarthy 91 function,
the option --check-measures=no is required to disable termination checks.
For solvers except for princess, the solver binary is expected to be present.
Since a custom version of Eldarica is in use here, it is packaged as a JAR file
in the repository.
Instructions are present in each example file as well. The corresponding auto-generated TIP files are available as examples on the Inox counterpart link.
We test mostly on Ubuntu; on Windows, you can get sufficient text-based Ubuntu environment by installing Windows Subsystem for Linux (e.g. wsl --install, then wsl --install -d ubuntu). Ensure you have a Java version ready (it can be headless); on Ubuntu sudo apt install openjdk-17-jdk-headless suffices.
Once ready, Download the latest stainless-dotty-standalone release for your platform. Unzip the archive, and run Stainless through the stainless script. Stainless expects a list of space-separated Scala files to verify but also has other Command-line Options.
To check if everything works, you may create a file named HelloStainless.scala next to the stainless 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 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.
If you see funny symbols instead of the beautiful ASCII art, run Stainless with --no-colors option for clean ASCII output with standardized error message format.
The release archive of Stainless only requires JDK17. In particular, it needs neither a Scala compiler nor SBT.
It is shipped with Z3 4.12.2, cvc5 1.0.8 and Princess. If Z3 API is not found, use option --solvers=smt-z3 to rely on the executable.
Alternatively, one may integrate Stainless with SBT. The supported Scala versions are 3.3.0 and 2.13.12
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.3.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 cvc5 can still be used if their executable can be found in the $PATH.
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-scalacfrontends/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.
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.
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, cvc5, and Princess.