GET IN TOUCH
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.
Research & Development
Software & Systems Analysis
Galois’s software correctness tools and techniques guarantee that your systems do exactly what you want, and no more.
WHY GALOIS?
In today’s complex, mission-critical environments, hidden defects and security gaps in software are an unaffordable liability. Traditional test-based validation techniques aren’t sufficient. Developers and evaluators need the ability to provide rigorous evidence of software correctness that supports that creation of enhanced functionality for demanding environments.
Galois’s Software and Systems Analysis (SSA) research team builds tools that increase the assurance of software systems and advance the state of the art in automated reasoning. These tools can discover emergent behavior in complex systems, or prove the absence of entire classes of defects backed by machine-checked mathematical proof. We are most well-known for developing the Software Analysis Workbench (SAW) and the Cryptol modeling language for cryptographic algorithms.
Beyond tool-building, we are experts in designing restricted software development paradigms that can ensure correctness and security by construction, either through API design, CI/CD integration, or the design and implementation of new programming languages and compiler pipelines.
Our guiding philosophy is to first identify the most impactful automated reasoning tool specific to a software system, security domain and cost structure. We then use existing technology when ideal tools already exist, and build new cutting-edge tools when they don't.
.png)
