Bolts: Stainless Verified Scala

This repository showcases examples of code verified using Stainless system for Scala. The benchmarks executed from run-tests.sh should run correctly with a recent main branch of Stainless and most are in this file.

Some highlights:

• Quite OK Image Format
• System F soundness (progress and preservation)
• Data structures, for example Conc Rope and Red-Black Tree with Remove
• Expression Compiler Correctness
• Algorithms of varrying complexity
• Functional Programming Principles, inspired by some of the Scala course labs
• Software foundations, inspired by Software Foundations book
• Examples from lectures and tutorials such as Lambda Days'20 keynote and ASPLOS'20 tutorial

Notable Stainless case studies outside of this repository include:

• From Verified Scala to STIX File System Embedded Code using Stainless
• Specification and Verification of a Blockchain Light Client