Romain Ruetschi

About me

Hi, my name is Romain Ruetschi, or just Romac.

I am a software engineer who strives to build correct and resilient software by standing on the shoulders of formal methods and programming language theory. I currently work at Informal Systems. Before that, I used to work at the Laboratory for Automated Reasoning and Analysis at EPFL.

My main areas of interest are related to formal verification of software, programming language theory, type theory, and compiler construction. I like exploring these topics in Rust, Scala and Haskell.

You can reach me on Twitter, Mastodon, or via Keybase.

Find me on


Formal verification of Scala programs with Stainless

@ Scala Romandie Meetup, Lausanne, October 2019

Formal verification of Scala programs with Stainless

@ Typelevel Summit Lausanne, June 2019

Refine your types!

@ Formal Methods & Verified Software Meetup, EPFL, May 2018

Formal verification of Scala code with Leon

@ Tokyo University, August 2015

Rust Workshop

# Co-presented with Dimiter Petrov
@ EPFL, Lausanne, November 2014



IBC relayer and library, in Rust.


Long-time contributor to Stainless, a verification framework for higher-order functional Scala programs developed at LARA at EPFL. Implemented support for typeclasses and ghost state, amongst other things.

Oxid (light)

Simple functional programming language with refinement types, powered by Inox. Crafted for my Refine your types! talk.


Rust implementation of Shamir & Adaptative threshold secret sharing schemes.

Rust implementation of a Merkle Tree.


mdash is a Chrome extension which replaces the New Tab page with a light dashboard linked with your bookmarks.

Hackers at EPFL

Hackers at EPFL was an association which aimed to promote the hacking culture at EPFL.