Formal verification of Scala programs with Stainless
summary
Demonstrates an engineering-ready verifier for a large subset of Scala that extracts to Inox + Z3/Princess, checks pre/postconditions and overflow/array bounds, and runs a termination checker; claims automatic proof of typeclass laws and gives a worked proof-by-induction for list append associativity. Shows several built artifacts: a verified parallel MapReduce pipeline, a verified RRB-like sequence, and an actor-system counter invariant proved inductively; integration includes an SBT plugin and ghost erasure so proofs incur no runtime cost.
AI-written summary · about
chapters (34)
- 0:00Introduction
- 0:28Outline
- 0:48What is Stainless
- 0:59Pure Scala
- 1:49Stainless
- 2:22Lower ring
- 2:47Inox
- 3:32Postconditions
- 3:59Math questions
- 4:43Static checks
- 5:17Termination checker
- 5:41Proofs
- 6:15Repetition
- 7:01Monoid
- 7:50Refresh Condition
- 9:05Associative
- 9:48Proof by induction
- 10:19Proof by inductive reasoning
- 10:37Stainless with support
- 11:00Stainless with no support
- 12:07Concrete implementation
- 13:20Actor systems
- 13:48Model
- 15:00Live Orient
- 16:10Wrapper
- 16:26More code
- 16:45Softlevel refinement types
- 17:12Sorted insert example
- 17:47Other features
- 18:20Upcoming features
- 18:58Skeleton 214 support
- 20:11More documentation
- 20:34Thanks
- 21:00Union types
related talks
40mSafe Coding with LLMs - Verifiable Scala Silver Bullet
38mGenerative Programming and Verification
36mAutograder for Functional Programming and Beyond
32mSafer Code with LLMs: Scala Types Silver Bullet?
48mPROBING THE UNPROVABLE AND PROVING THE IMPROBABLE
52mWhat logic can teach us, Scala programmers
41mReconstructing Scala
19mExecuting Certified Model Transformations on Apache Spark