I'm a research engineer at Nokia Bell Labs, currently working on distributed systems with Scala. During this work, and sometimes in my free time, I occasionally contribute to open source Scala libraries (like shapeless or Cats).
While a lot of software systems implement and use finite-state machines, the correctness of the state transitions and operations is usually not statically verified. We present a Scala library, which allows defining statically verified domain-specific languages (DSLs) for working with state machines. Our library enables the compile-time checking of the implementation of these DSLs, by encoding states into Scala types, and using an indexed free monad and a type class for restricting state transitions.