• Stars
    star
    356
  • Rank 119,446 (Top 3 %)
  • Language
    Scala
  • License
    Apache License 2.0
  • Created over 8 years ago
  • Updated 24 days ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

Verification framework and tool for higher-order Scala programs

Stainless Release Nightly Build Status Build Status Gitter chat Apache 2.0 License

Verification framework for a subset of the Scala programming language. See

Quick start

Download the latest stainless-dotty-standalone release for your platform. Unzip the archive, and run Stainless through the stainless.sh (or stainless.bat) script. Stainless expects a list of space-separated Scala files to verify.

To check if everything works, you may create a file named HelloStainless.scala next to the stainless.sh 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.sh 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.

This archive of Stainless only requires JDK17. In particular, it needs neither a Scala compiler nor SBT. It is shipped with Z3 4.8.14 and Princess.

SBT Stainless plugin

Alternatively, one may integrate Stainless with SBT. The supported Scala versions are 3.2.0 and 2.13.6 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.2.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 CVC4 can still be used if their executable can be found in the $PATH.

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:

  • frontends/scalac/target/universal/stage/bin/stainless-scalac
  • frontends/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.

Further Documentation and Learning Materials

To get started, see videos:

or see local documentation chapters, such as:

There is also a Stainless EPFL Page.

License

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, CVC4, and Princess.

More Repositories

1

leon

The Leon system for verification, synthesis, repair
Scala
162
star
2

ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Scala
122
star
3

inox

Solver for higher-order functional programs, used by Stainless
Scala
88
star
4

scallion

LL(1) parser combinators in Scala
Scala
56
star
5

smart

Verification and Generation of Smart Contracts using Stainless and Scala
HTML
35
star
6

lisa

Proof assistant based on first-order logic and set theory
Scala
33
star
7

treenet

Recursive Neural Networks for PyTorch
Python
31
star
8

bolts

Bolts: Stainless Verified Scala Examples
Scala
17
star
9

nugget

Neural-Network Guided Expression Transformation
Python
12
star
10

jahob

Jahob Verification System
C
11
star
11

comfusy

Implementation of the "Complete Functional Synthesis" approach described in the eponymous PLDI 2010 paper.
Scala
11
star
12

silex

Lexing library for Scala
Scala
10
star
13

welder

Interactive Theorem Proving based on Inox
Scala
10
star
14

SystemFR

System FR: Formalized Foundations for Stainless
Coq
9
star
15

scallion-proofs

Proofs of correctness for Scallion (https://github.com/epfl-lara/scallion)
Coq
9
star
16

rust-stainless

An experimental Rust frontend for Stainless
Rust
6
star
17

StainlessFit

Stainless directly built on System FR, with standalone front-end
Scala
5
star
18

OCBSL

A minimal algorithm to decide the word problem in Orthocomplemented Bisemilattices, in Scala.
Scala
4
star
19

verified-2048

A 2048 clone verified by Stainless
Scala
4
star
20

actors-in-stainless

Actor System library for Stainless which runs on Akka
Scala
4
star
21

asplos2022tutorial

ASPLOS 2022 Tutorial on Stainless
C
4
star
22

fit-code

TypeScript
3
star
23

muscat

A unit testing framework for concurrent Scala programs
Scala
3
star
24

stainless-project.g8

Giter8 template for Stainless-enabled projects
Scala
3
star
25

verifythis2020

VerifyThis2020 Challenge in Stainless
Scala
2
star
26

lattices-algorithms

This repository contains two algorithms for the word problem and normalization problem of Ortholattices and Orthocomplemented Bisemilattices
Scala
2
star
27

silex-proofs

Proofs on lexing with derivatives and zippers
Coq
2
star
28

cs550

Scala
2
star
29

compiler2024-labs-public

Scala
2
star
30

leon-web

Web-interface for Leon
Scala
2
star
31

GrammarComparison

A System for Analyzing and Comparing Context-Free Grammars
Scala
2
star
32

grammar-web

An online tutoring system for context-free grammars
Scala
2
star
33

scala-native-stainless-sample

Scala
1
star
34

funprog-lambda

Scala
1
star
35

STIX-showcase

Scala
1
star
36

Deep_Learning_On_Code_With_A_Graph_Vocabulary

Code to reproduce the experiments in the paper Deep Learning On Code With A Graph Vocabulary
Python
1
star
37

verified-lambda

A verified lambda interpreter
Scala
1
star