Our R&D Capabilities

At Galois, we believe trustworthy systems are built on a formal mathematical foundation. Core to this is the application of formal analysis techniques that allow systems to be modeled, analyzed, and proven to have important properties. We use functional programming language technologies that facilitate such formal analysis as well as providing flexibility to build specialized languages for solving and analyzing domain-specific problems.

Our researchers and engineers also apply this formalized approach to the design of software systems where a high degree of trust is placed in the systems to do exactly what they are intended, and no more. And in the realm of embedded systems, our researchers build on their expertise in language design, static analysis, and formal methods in order to build tools that increase the reliability and simplify the design of complex embedded systems.

More About Our Approach

  • Formal Methods
  • Galois' formal methods team has world-class expertise in using theorem provers, model checkers, rewriters, and other formal methods tools to develop high assurance software.

  • Functional Programming
  • Galois’ programming languages research is built on functional programming concepts and provides insights and techniques to address the problems stemming from the complexity of business- and mission-critical systems.

  • Domain-specific Languages
  • In the world of highly complex, non-uniform critical systems, domain area experts are challenged with understanding the system in a way in which they can have confidence in its reliability and security. One solution Galois employs to address this challenge is the development of domain-specific languages (DSL) to translate the system language to the problem-space language in terms that can be understood by both sides.

  • Embedded Systems
  • Galois provides a range of services in high-assurance embedded system development. We leverage our expertise in formal verification, run-time monitoring, security, and safety to bring new approaches to the area.

  • Systems Software
  • Galois' systems software offer trusted and assured implementations of many systems components — network stacks, hypervisors, file systems, and device drivers — allowing you to step away from bugging/legacy systems components and replace them with our systems written in high-level languages.


Our Technical Areas


We are a leader in the ground-breaking process of computing on data while it remains encrypted, and in the automated generation, validation and synthesis of high assurance cryptographic solutions.


Open Source

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.

Select Repositories

  • SAW

    The Software Analysis Workbench (SAW) is a set of tools developed for extracting formal models from existing code, enabling developers and security analysts to reason about and prove program properties. SAW is able to show that a program satisfies a functional spec and avoids undefined behavior.

  • SMACCMPilot

    SMACCMPilot is an embedded systems software research project where we are building open-source autopilot software for small unmanned aerial vehicles (UAVs) using new high-assurance software methods.

  • Copilot

    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 can be used to develop a variety of functional-style embedded code.

  • Cryptol

    Cryptol is a domain-specific language for specifying cryptographic algorithms. Cryptol version 2 is now released as open source under a 3-clause BSD license. Our goal is that it becomes a widely adopted standard for expressing cryptographic algorithms.

  • HaLVM

    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.”

  • BLT

    BLT is a C/C++ library for solving certain integer linear programming (ILP) problems using techniques that come from the theory of lattices.