Software & Projects

Isabelle/jEdit window


A list of my Isabelle-related projects can be found here.
Screenshot of Isabelle/jEdit: License of Isabelle, License of jEdit
Typelevel homepage


Contributor to & maintainer of various Typelevel projects, including:

Screenshot of, Copyright © 2013–2017 its contributors
Logo of FFFUU

Fancy Formal Firewall Universal Understander

Contributor to Cornelius Diekmann's Haskell tool (and corresponding formalization) to simplify iptables firewall rulesets. The research papers can be found here.
Diagram by Cornelius Diekmann
Leon interface


I have developed an extension to Leon that allows it to use Isabelle as a solver in the background. The research paper can be found here. The major challenges were system integration (this has since been extracted as a separate project, libisabelle) and translating Scala expressions into idiomatic Isabelle/HOL definitions without compromising correctness.