Verification framework for a subset of the Scala programming language. Supports contract-driven verification as well as termination checking of higher-order functional programs with local imperative features (see Pure Scala and Imperative for more details about the supported fragment).
To get started, see the documentation chapters, such as
- Installation
- Getting Started
- Introduction to Stainless
- Stainless EPFL Page
- Viktor's keynote at ScalaDays 2017 Copenhagen
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.
Relation to Leon
The Stainless/Inox stack has grown out of the Leon codebase and subsumes the verification and termination checking features of Leon. The new projects aim to provide a more stable and principled implementation of the verification techniques underlying Leon. Feature-wise, Stainless has already outgrown Leon verification and provides new features such as higher-order contracts and contract-based termination checking.