Samuel Chassot
Portrait of Samuel Chassot
Formal Verification Programming Languages Scala / Stainless

Samuel Chassot

PhD candidate at LARA, EPFL, advised by Prof. Viktor Kunčak

I work on making software verification practical and accessible — building verified libraries and improving the tools used to prove real-world code correct.

Email GitHub ORCID Scholar CV

About

My name is Samuel Chassot. I am a PhD candidate in LARA at EPFL, Switzerland, under the guidance of Prof. Viktor Kunčak. My research focuses on Formal Methods and Software Verification.

Before starting my PhD, I obtained an MSc in Computer Science from EPFL, Switzerland.

Outside of my academic pursuits, I am a passionate watchmaking enthusiast, learning and practicing this craft during my leisure time. I am also passionate about space exploration, astronomy, and everything aerospace and aviation related.

Research

My current research focuses on software verification, particularly with Stainless, a verifier for a subset of Scala that uses SMT solvers to find counterexamples or prove validity.

My thesis, in one line: make software verification accessible.

Build verified software

A growing library of verified data structures, regex engines, and frameworks — proven correct, not just tested.

Build better tools

Improving verifiers like Stainless so that proving real-world code correct takes less expert effort.

Much of my verification work is open source in Bolts, a library of verified data structures, algorithms, and programs proven correct with Stainless.

Bolts on GitHub

Recent projects

Verifying the Scala standard library's LongMap

Full verification of a mutable, open-addressing hashtable from the Scala standard library. The proof uncovered a bug in the original implementation; my formally verified fix was accepted upstream. Published at IJCAR 2024.

Paper

Verified regex matching & invertible lexing

An implementation of regex matching with derivatives, verified in Stainless, used to build a lexer proven correct: it follows longest-match semantics and is invertible.

Verified ASN.1 serialization, with ESA

Verification of an ASN.1/ACN serialization protocol implementation, in collaboration with the European Space Agency. Published at VMCAI 2025.

Paper

Earlier projects

SVSHI — Secure and Verified Smart Home Infrastructure

My master thesis. SVSHI formally verifies Python smart building apps for KNX devices and manages KNX communications: a framework to develop and verify applications, plus a runtime system to run them on a KNX infrastructure.

GitHub

Resource interfaces

An exploration of resource interfaces for programs — analogous to semantic interfaces, but expressing resource usage as a function of inputs — with a focus on serverless computing and a Python prototype extracting basic interfaces for simple programs.

Report

Publications

Talks

  • Refinement Types in Scala with Stainless
    With Katarzyna Marek and Matt Bovel — Scala Workshop 2026
    Details Slides
  • Mutable Cells for Memoized Lexing
    Verified memoization framework for verified invertible lexing — invited talk, VIMPL 2026
    Slides
  • To Space and Back: Verified Serialisation
    Formally verifiable generated ASN.1/ACN encoders and decoders — VMCAI 2025
    Slides
  • Stainless Verifier and Composition in Verification
    LMF Seminar on Software Verification, 2024
    Slides
  • Verifying a Realistic Mutable Hash Table
    IJCAR 2024
    Slides

Miscellaneous Resources

Interesting SMT queries

Interesting SMT queries I encountered in my projects. They can serve as benchmarks.

A slow cvc5 query

Generated by Stainless when verifying a "Bit Stream" implementation for the ASN.1 project. It takes a particularly long time to solve: ~100 s on my MacBook Pro, ~230 s on our Linux server. The smt2 file contains a comment header with options to pass to cvc5.

smt2 file