Galois, Inc.

In a recent (excellent) The Wall Street Journal article, Journalist Belle Lin explored how Amazon is using automated reasoning to tackle the problem of AI hallucinations head-on. Galois's work proving correctness of AWS cryptography is mentioned! Automated reasoning is a subset of formal methods – Galois’s bread and butter. Since 2015, Galois has worked with AWS to help ensure the security of some of the key cryptographic systems that protect their cloud. AWS’s customers include start-ups, large enterprises, and leading government agencies in more than 245 countries. Our work with AWS has yielded the highest possible level of continuous protection for a large percentage of the world’s most valuable and most critical data. That means that Galois has played a key role in securing financial transactions that keep the global economy churning, state secrets that keep citizens safe, and the privacy of personal communications. This is real, tangible impact at the highest level—all thanks to applied math. Now, Galois is working with DARPA to better understand the inner workings of Generative AI. Why it works when it works, why it fails when it fails, and how to achieve predictable, bounded AI behavior. Stay tuned. 

Galois's RDE framework revolutionizes defense system development, reducing timelines and increasing confidence. Learn how this model-based approach enables rapid capability deployment without compromising on quality or security.

Galois was awarded $12.6 million by DARPA for HEIMDALLR (Hybrid Electromagnetic side-channel and Interactive-proof Methods to Detect and Amend LogicaL Rifts) to support the COOP (Continuous-correctness On Opaque Processors) program. Today, although mission critical software (MCS) in DoD equipment may be heavily tested or even formally proven correct, the correct execution of that software remains at risk due to interactions with the physical and software environment on which it runs. Currently, it is very difficult to assure trust about that external environment, which includes the processor and memory on which the software runs, because you only have control over the MCS. It is also difficult to assure trust about other portions of the software stack, such as the operating system and other programs that run in the same environment, which are likely commercial or otherwise “off-the-shelf”. With HEIMDALLR, Galois aims to solve this problem through an alternative approach that combines the power of formally-verifiable computation, rather than formally verified software, with the use of electromagnetic side-channel sensing to assure that errors in program flow or computation are provably identified, isolated, and corrected during execution. Learn more in our latest!

Over the winter break, OpenAI announced their new model, o3. Much of the media attention rightly focused on its impressive results on the ARC-AGI benchmark, but for us at Galois, the most significant result was something else—the model’s 25% score on a benchmark called Frontier Math. Learn more in our latest article by Mike Dodds:

Galois is excited to announce that we are kicking off a project to verify the frontend of the Jolt zkVM, with financial support provided by a grant from the Ethereum Foundation.

Complex systems, like aircraft, are notoriously difficult to modify quickly and safely. Could Rigorous Digital Engineering (RDE) offer a solution? We tested this approach on a SuperVolo UAV to see if it could help us swap out a component with full understanding of the impact of that change on safety and performance. If successful, this approach could be applied to bigger and more complicated cyber-physical systems, potentially save the DOD billions, and transform the future of engineering. Learn more in our latest animated video:

As 2024 comes to a close and a new year begins, we’re excited to reflect on a great year at Galois that saw groundbreaking research projects, innovative software releases, and impactful new collaborations. We love what we do, and it’s fun to share highlights made possible by working well together! Give our 2024 Highlights article a read to learn more about what we've been up to!

Galois has a new website! We're kicking off the new year with a new look and (just as exciting) a new way of organizing how we communicate our research, solutions, and story. Take a look!

As we spend time with family and friends this Holiday Season, we are grateful for the wonderful community not only within our company, but within our amazing spinouts! Galois has helped launch several innovative companies now driving impact in a variety of fields, and we're proud of them. So join us in raising a toast to ExistX, Tangram Flex, Niobium Microsystems, TOZ, thatDot, and Free & Fair. Happy Holidays!

With the CAMDEN project, Galois is exploring the use of mechanism design as a solution to effectively incentivize and accelerate collaboration in critical DoD domains, including export control strategies for supply chain security, natural disaster and pandemic response, cyber deterrence, and especially the defense acquisition process. Each of these areas is fraught with unique and thorny complexities. We’re looking to study them closely, model and simulate the human decision-making behavior at the heart of each, and then explore how different variables can be changed to push that behavior in one direction or another. Ultimately, our goal is to build one or more deployable mechanisms to serve as a generalizable solution: a dynamic software program to model incentive structures for optimal design of complex systems. Learn more in our latest article by Galois Principal Scientist David Burke