Hosted at https://github.com/epfl-lara/stainless ; mirrored at https://gitlab.epfl.ch/lara/stainless . Check out also Inox and Bolts.
Verification framework for a subset of the Scala programming language. See the tutorial.
Please note that this repository uses git submodules, so you need to either:
- clone it with the
--recursiveoption, or - run
$ git submodule update --init --recursiveafter cloning.
Please note that Stainless does not support Scala 2 frontend anymore, only Scala 3.5.0 and later. The latest release that supports Scala 2.13 frontend is the v0.9.8.7.
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 beautiful ASCII art, run Stainless with the --no-colors option for clean ASCII output with a standardized error message format.
The release archive of Stainless only requires JDK 17. In particular, it needs
neither a Scala compiler nor SBT. It is shipped with Z3 4.12.2+, cvc5 1.0.8+ and
Princess (branch compiled for Scala 3). If the Z3 native API is not found, use
the option --solvers=smt-z3 to rely on the executable instead of API call to
z3.
Please refer to the installation documentation here.
The main documentation for Stainless is hosted at https://epfl-lara.github.io/stainless/.
To get started with using Stainless, see videos:
- Stainless Introduction for 2nd year EPFL BSc students
- ASPLOS'22 tutorial
- FMCAD'21 tutorial
- Formal Verification Course:
- Getting Started
- Four part tutorial: 1, 2, 3, 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 which hosts a mirror of the GitHub repository.
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.
