Projects

• Choreo

  Choreographic programming in Scala

  Status: Active

• itf-rs

  Rust library for consuming Apalache ITF traces

  Status: Active

• Quint

  Contributor to Quint, an executable specification language based on the temporal logic of actions (TLA)

  Status: Active

• Hermes

  IBC relayer and library, in Rust.

  Status: Active

• Stainless

  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.

  Status: Past

• Oxid (light)

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

  Status: Prototype

• RustySecrets

  Rust implementation of Shamir & Adaptative threshold secret sharing schemes.

  Status: Inactive

• merkle.rs

  Rust implementation of a Merkle Tree.

  Status: Inactive

• mdash

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

  Status: Abandoned

• Hackers at EPFL

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

  Status: Past