Open source software
Fancy Formal Firewall Universal Understander
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.