Stainless
Stainless is a tool for verifying Scala programs. Stainless is developed by LARA at EPFL’s School of Computer and Communication Sciences. Stainless can verify that your program is correct for all inputs, it can report inputs for which your program fails when they exist, and it can prove that functions do not loop. Using Stainless before running or deploying the software can eliminate crashes, logical errors, security flaws, and other defects.
Main Links
- GitHub
- Releases (only requires OpenJDK JRE 8 or above)
- Installation instructions (standalone, Docker, sbt, Metals)
- Documentation
Why Stainless
Stainless is a way to use Scala to develop highly reliable applications, with errors caught early during the development process. Thanks to its use of formal proofs, Stainless can establish safety and termination properties using symbolic reasoning, covering infinitely many inputs in a single run of verification.
One can compare Stainless to proof assistants such as Isabelle/HOL, Coq, or ACL2 in terms of the complexity of some of the program properties it can prove, though it was originally conceived more as a program verifier, such as Dafny. Stainless can be more automated when finding proofs of programs compared to proof assistants, and can also report counter-examples for invalid properties in many non-trivial cases, see counter-examples for bugs in benchmarks such as ConcRope.scala, ListOperations.scala, Mean.scala, PropositionalLogic.scala, AssociativityProperties.scala, InsertionSort.scala, more example reports, or check some of our regression tests. On the other hand, proof assistants are much better at formalizing mathematics than Stainless, especially when it comes to libraries of formalized knowledge.
What Stainless Verifies
Stainless supports verifying:
- Assertions which should hold at the place where they are stated, but are checked statically
- Postconditions using ensuring function: assertions for return values of functions
- Preconditions using require function: assertions on function parameters
- Loop invariants: inductive assertions that hold in each loop iteration after the while condition check passes
- Algebraic data type class invariants: assertions on immutable parameters of constructors (which remain true for all constructed values)
- Automatic checks done for the absence of runtime failures: completeness of pattern matching, division by zero, array bounds checks, map domain checks
Stainless ensures that the input program belongs to a subset of Scala. This subset syntactically prevents:
- the creation of null values or unininitalized local variables or fields (therefore, dereferencing fields in Stainless programs cannot lead to null dereference error)
- explicitly throwing an exception.
The choice of the subset of Scala along with the checks for runtime errors rules out most known sources of errors in Scala programs. An exception are resource exhaustion errors (but see resource bound analysis in Leon documentation below).
Stainless correctly models integral types such as Int with an appropriate level of bits and takes overflow into account (for unbounded integers, use BigInt).
Stainless performs non-trivial termination checks for its functions and supports specifying decreasing measure functions.
Inox
Stainless derives its verification power from the Inox constraint solver for purely functional recursive constraints:
Inox makes use of SMT solvers Z3, CVC4, and Princess, and adds support for recursion, higher-order functions, its own support for quantifiers, as well as a form of dependent types.