This summer, I had the opportunity to join Galois as a Research Engineer through the Hiring our Heroes Fellowship Program. Hiring our Heroes is part of the Department of War SkillBridge program that allows active-duty service members to work in industry during their last 180 days in the military. The service member can see what work-life is like outside of the military, while using their military…

In January 2024, we highlighted the latest release of Swanky, our suite of Rust libraries for secure computation. Since then we’ve made many changes to the codebase, both in terms of improving overall code quality and documentation, alongside new capabilities. It’s been a while since we’ve provided an update on these changes, so think of this as our biennial blog post on how things are going. And…

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. Frontier Math is designed to measure human-like mathematical abilities in an AI. Before o3, generative AIs were sc…

Building secure communication systems requires both secure cryptographic primitives and also secure cryptographic protocols that build messaging schemes on top of those primitives. Well-designed protocols are the backbone of almost all modern digital communication, enabling key exchange, entity authentication, secure channels, and anonymous messaging. On the other hand, improperly designed protoc…

This article is a companion piece to Specifications Don't Exist. It began life as part of a talk I gave in late 2024. I love formal methods—I should say that to begin with, because this article is mostly about what doesn’t work when trying to do FM projects. Over the last 20 years, formal methods have grown and grown, and I’m proud to say that Galois has made its own contributions to this success…

Galois’s mission is to help make the critical systems that the world relies on more secure and trustworthy. Over the years, we’ve put our team’s deep expertise in software correctness, cryptography, digital engineering, and machine learning to work, providing formal assurance for complex systems in high stakes contexts for both government and commercial clients. From militaries to financial insti…

This article is a companion piece to What Works (and Doesn't) Selling Formal Methods. It began life as part of a talk I gave in late 2024. Some things are difficult, and some things are merely expensive. Imagine this: aliens are coming to kill us all. Humanity sends its best negotiators, and the aliens announce that they will call off their horrible assault only if we release a formally verified …

At Galois, we’re always looking for better ways to build reliable systems. A big part of that is doing our own research. At 130 people, we’re one of the world’s largest formal methods research teams! But another part of our work is understanding new tools and techniques from the research community. We’re interested in solving problems using any approach that works, including learning from other f…

In his 1900 book The Wonderful Wizard of Oz, L. Frank Baum tells a story that will resonate with any software engineer. A woodman by the name of Nick Chopper suffers a series of workplace accidents. In turn, his arms, legs, body, and even his head are replaced by metal prosthetics. Eventually, what remains is an entirely different man made of tin. Like Baum’s Tin Man, all software projects are re…

System engineering involves a delicate interplay between three tasks: specification (what a system should do); implementation (what a system actually does); and verification (determining whether they agree). Already, novel generative AI technologies have emerged that can assist with implementation and verification (e.g., respectively, Microsoft’s CoPilot, and formal verification tools developed o…

“Foolish consistency,” Emerson claimed, “... is the hobgoblin of little minds.” We agree! The problem, in both philosophy and distributed computing, is to figure out when consistency is foolish and when it is absolutely necessary. Fortunately, formal methods technologies can help us address this problem. Galois and our partner Twisp have been using the P language for systematic concurrency testin…

We think that Rust is a great language, and maybe you agree! Unfortunately, even if you do, there’s a good chance whatever application you’re working on is written in some older language such as C. To help with this, Galois has been developing c2rust, an automated transpiler (source-to-source translator) from C code into Rust code. c2rust can take almost any C and turn it into C-like Rust code, t…

Let me get right to the point without any nonsense about aliens: Interactive theorem proving tools such as Lean are the most powerful and trustworthy kind of formal methods tool. They have been used to formally verify important things such as cryptographic libraries, compilers, and operating systems. Unfortunately, even experts find ITP proofs time-consuming and error-prone. That’s why it’s excit…

Many of the verification and static analysis tools we build at Galois are based on the same technology: a symbolic execution engine for a language called Crucible. There are a lot of advantages to doing this. It’s what makes it possible for SAW to reason about C, C++, Rust, and x86 assembly, all through the same interface, just by translating into Crucible. Improvements to Crucible improve all ou…

AI is pushing software into an industrial age, but formal verification infrastructure is still operating like a guild craft. For decades, formal verification thrived in university basements and research labs. We wrote arcane Rocq tactics, built bespoke proofs, and spoke in theorem provers few outsiders could understand. Verified systems are still rare, expensive, and mostly isolated from one anot…

Zero-knowledge proofs (ZKPs) are an emerging cryptographic technique on the verge of becoming increasingly useful and important for everyday users in the near future. In a ZKP, one party can prove to another that they know a statement is true without revealing any other information. It ensures trust and verification in cryptographic transactions while maintaining privacy and security. Recent work…

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. Zero-knowledge virtual machines (zkVMs) emulate program executions in ZK, enabling verifiers to validate a program’s execution faster than it takes to rerun the computation – improving scalability and privacy. These power…

Software supply chain attacks are on the rise, increasing a staggering 742% per year on average since 2019. Sometimes called “third party attacks,” these cyberattacks infiltrate third party or open source software libraries with malicious code, infecting vendors and components along the software supply chain. These days, any given software artifact may depend on hundreds or even thousands of thir…

I’m excited to announce our paper “ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification” has been accepted to PLDI 2022. Programs often need to reveal information about private or sensitive data. For example, consider an advertiser who wants to send an advertisement to users near a restaurant. To accomplish this, the advertiser could write a query asking a social med…

Over the last few months, Galois has published or spoken about a variety of technologies based on the open source Xen hypervisor: our port of FreeRTOS on Xen, our MAC-enhanced version of the XenStore, and, of course, our continuing work on the Haskell Lightweight Virtual Machine (a.k.a., the HaLVM). Based on all this activity, I get asked the obvious question: Why is Xen so compelling to Galois? …