Our team has world-class expertise in using logical frameworks, automated theorem provers, model checkers, rewriters, and other formal methods tools to gain measurable proof that software is correct and secure.
Our tools automatically generate code based on high level specifications. This allows us to gain measurable guarantees that the resulting software does only what it is intended to do, and is free of a wide range of errors and vulnerabilities.
Our programming languages research and development provides unique advantages to address the problems of highly complex, non-uniform critical systems. We also develop domain-specific languages (DSLs) that enable domain area experts to express their goals in problem-space language, and have confidence in the systems’ reliability and security.
By focusing on fundamental components that are critical to security and reliability—like network stacks, operating systems, hypervisors, and file systems—we enable our clients to cement trustworthiness in the foundation of critical systems.
We design secure, reliable, efficient bespoke semiconductor solutions to your most difficult computing problems for systems from the network edge to the data center.
We focus on 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.
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.
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 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 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 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.
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.”
We take pride in personally connecting with all interested partners, collaborators and potential clients. Please email us with a brief description of how you would like to be connected with Galois and we will do our best to respond within one business day.