Our software correctness tools guarantee that your systems do exactly what you want, and no more.Explore
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 correct.
Our researchers and engineers apply this formalized approach to the design of critical software systems, systems that must do exactly what they are intended, and no more. This rigorous systems engineering method allows us to mathematically prove that a system behaves exactly as we intend under all circumstances.
More About Our Approach
- Formal verification
- Code that is correct and secure by default
- Powerful programming languages
- Focus on fundamentals
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.×
Our Technical Areas
We design secure, reliable, efficient bespoke semiconductor solutions to your most difficult computing problems for systems from the network edge to the data center.Explore
We build tools that empower our clients to map and understand the minute components and interactions of complex system architecture.Explore
We focus on the groundbreaking processes of securely linking and computing on private data; securely proving computation is done correctly; and on the creation, validation, and synthesis of high-assurance cryptographic solutions, including quantum-resilient (“post-quantum”) schemes.Explore
We develop new technologies that guarantee the confidentiality, integrity, and availability of your systems.Explore
We build tools to increase reliability and simplify the design of complex embedded systems.Explore
We combine formal methods with cutting-edge machine learning techniques and tools, empowering our clients to leverage the full potential of their data sets and solve complex problems.Explore
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.”
BLT is a C/C++ library for solving certain integer linear programming (ILP) problems using techniques that come from the theory of lattices.