Open Source at Galois

The open source culture, much like Galois’ own organizational model, thrives on the power of collaboration. Galois benefits from advances made in the open source community and we strive to continually give back, making much of our software freely available to others. This page lists some of our open source contributions.

Haskell libraries and tools

In the course of projects at Galois, we have developed a large number of open source libraries for the Haskell language. We host upstream repositories at on github.

Many other open source libraries are available on the Haskell central library archive, Hackage, including:

  • cabal-dev - a sandboxed Haskell build environment
  • utf8-string - a UTF8 layer for IO and Strings
  • xml  - a simple XML library
  • sqlite - a binding to sqlite3
  • json - JavaScript Object Notation for Haskell
  • feed - interfacing with RSS (v 0.9x, 2.x, 1.0) + Atom feeds
  • selenium - communicate with a Selenium Remote Control server
  • SHA - the SHA suite of message digest functions
  • RSA - the RSA encryption and signature algorithms
  • delicious - the social tagging site's API
  • mime - support for working with MIME types
  • strict-concurrency - strict versions of some standard Haskell concurrency abstractions
  • cereal - a binary serialization library
  • curl - a client-side URL transfer library
  • BoundedChan - channels guaranteed to contain no more than a certain number of elements
  • http-server - a library for writing Haskell web servers


The HaLVM is a port of the GHC runtime system to the Xen hypervisor, allowing programmers to create Haskell programs that run directly on Xen’s “bare metal.” 

HaLVM is available on github.


HaLFS is a filesystem implemented in the functional programming language Haskell. HaLFS can be mounted and used like any other Linux filesystem, or used as a library. HaLFS is a fork (and a port) of the filesystem developed by Galois.

HaLFS is available on github.

Isabelle ismt tactic

The ismt package allows Isabelle to invoke SRI Inc.’s Yices SMT solver to automatically prove or refute formulas written in the subset of higher order logic that Yices understands. When Yices refutes a formula, the ismt package can also convert the Yices-produced counterexample back into a higher order logic formula.

The tactic is available at the ismt home.


Copilot is a domain specific language for writing embedded C code. The package includes an interpreter, a compiler, and uses a model-checker to check the correctness of your program. Copilot was originally developed to write embedded monitors for more complex embedded systems, but it can be used to develop a variety of functional-style embedded code.

Copilot is available on Hackage.


Orc is a concurrent scripting language, available as an embedded DSL in Haskell. Orc is the combination of three things: many-valued concurrency, external actions (effects), and managed resources, all packaged in a high-level set of abstractions that feel more like scripting rather than programming. It provides a very flexible way to manage multiple concurrent actions, like querying remote web sites, along with timeouts and default actions.

Orc is available on Hackage.


Nettle is a domain specific language for routing and configuration. Using Nettle it is possible to express new network routing policy languages that can be translated into lower-level protocols such as BGP. 

Nettle packages are available on Hackage (nettle-frpnettle-openflow).


FiveUI is a framework and tool for checking web-based user interfaces against codified UI guidelines. It is the first step towards an extensible, semantically aware, reusable, and pragmatic toolchain for checking aspects of user interfaces against arbitrary guidelines.

FiveUI is available on github.