Verification framework for a subset of the Scala programming language. See
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:
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.
Stainless is released under the Apache 2.0 license. See the LICENSE file for more information.
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.