This summer, as part of a project verifying the frontend of the Jolt zkVM, Galois intern Liza Pertseva and her team used an SMT solver to automate Lean proofs, saving over 6,800 lines of Lean code that would have been otherwise written by hand. Learn more: www.galois.com/articles/aut...

This summer, our returning intern – Cornell PhD student Mark Moeller – helped show how Galois’s 5STARS tool could prevent a simulated hospital cyberattack before it ever began. Read more: www.galois.com/articles/gal...

Once someone understands what formal methods are, their next question is typically "Where do I put them?" Our latest explainer digs in: www.galois.com/where-do-i-p...

Interactive Theorem Proving is time-consuming, tedious, and just plain hard. So, Galois Principal Scientist @m-dodds.bsky.social tried using Claude Code for ITP. Surprisingly, IT WORKED (with some big caveats)! Give the full article a read to learn more: www.galois.com/articles/cla...

"It’s the people that have made my time here so special," said Galois intern Angel Gallegos. "Galois is full of really smart people, but everyone is down-to-earth and happy to talk. You’re always learning something new." Read more in our Q&A with Angel: www.galois.com/articles/gal...

Big LLMs are great... unless you're working with sensitive data. Galois intern Kevin Fisher spent the summer exploring how far local LLMs can go in code generation without sacrificing privacy. Read Kevin's full writeup here 👇 www.galois.com/articles/pri...

Big news: Brad Martin has joined Galois as our newest principal scientist! After nearly 40 years in federal service, Brad is bringing his vision + expertise in formal methods & cybersecurity to help us tackle some of the world’s biggest tech challenges. Welcome to the team, Brad!

This summer, Galois intern @binarynewts.bsky.social explored how LLMs could help translate legacy C code into safe Rust. Their project, CNnotator, generates memory safety annotations for C code. Learn more: galois.com/articles/esc...

Evaluating FHE program performance used to take weeks of trial-and-error. Dioptra (open-source from Galois) streamlines this process—estimating time & memory usage for OpenFHE Python programs, with performance models & comparisons to guide better decisions. 🔗 www.galois.com/articles/gal...

"Galois is unlike any place I’ve worked before," writes Galois intern Mariana Ferreira. "There is a remarkable level of humility across the organization. Titles and hierarchies take a backseat to curiosity, kindness, and collaboration." Read more: www.galois.com/articles/ref...

Congrats to Galwegians Scott Moore, David Darais & Sourya Dey (and former Galwegians Ethan Lew & Ramy Tadros) on “A Simulated Reconstruction and Reidentification Attack on the 2010 U.S. Census” being accepted at Harvard Data Science Review. Read more: hdsr.mitpress.mit.edu/pub/ntchx9im...

🚨 Paper accepted! Congrats to Galwegians Santiago Cuéllar, James Parker, Stuart Pernsteiner + co-authors Bill Harris, Ian Sweet & Eran Tromer on "Cheesecloth: ZK Proofs of Real-World Vulnerabilities” being accepted for publication in ACM TOPS! Read it!: dl.acm.org/doi/10.1145/...

Galois Principal Scientist @m-dodds.bsky.social's latest on formal specifications, informal specifications, and the inescapable burden of having to clarify our ideas. Give it a read! www.galois.com/articles/specifications-dont-exist

“[Formal methods] advancements enable us to scale secure software systems across all DOD, from legacy platforms to cutting edge AI and hypersonic technologies defending our digital landscape." - HON. Emil Michal, Undersecretary of Defense for Research and Engineering youtu.be/ROZv0G-6zxs?...

🎉 Shout out to Galois intern Mark Moeller, who (with coathors) is presenting his paper “Active Learning of Symbolic NetKAT Automata” at #PLDI2025 in Seoul on Wed, June 18! If you’re at PLDI, swing by to say “Hi,” chat about Galois, and nerd out on automata & #NetKAT for packet-switched networks!

Congrats to Galois Research Engineer Ariel Kellison, who recently won the Frederick A. Howes Scholar in Computational Science Award, which honors exceptional leadership, character, and technical achievement in the field of computational science!

At Galois, we often say things like: “Formal methods form the backbone of everything we do.” But what exactly are formal methods? How do they work, and why are they so important? We created a handy reference page to explain: www.galois.com/what-are-for...

"Curiosity is at the core of who we are," says Galwegian Anne Marie McClaran. Our Principal Scientists drive their own research agendas, following their curiosity to push their disciplines forward and solve real-world problems.

From helping NASA make space exploration safer to securing financial transactions to safeguarding the privacy of everyday communications — Galois is proving the safety of the systems the world depends on. Applied math, real-world impact. Dive in: www.galois.com/articles/the...

What actually works when selling formal methods in industry? What doesn't? The way Galois Principal Scientist @m-dodds.bsky.social sees it, many FM projects don’t pencil out not because clients are irrational, but because the cost/benefit tradeoffs don’t make sense. www.galois.com/articles/wha...

“If you can get that in this life — having work you're really passionate about, that you think is important, and working with people you really like — that's kind of a magic combination,” says Galois Principal Scientist @m-dodds.bsky.social. Learn more: www.youtube.com/watch?v=FNYo...

We're excited to share our work on BRACELET, part of DARPA's Enhanced SBOM for Optimized Software Sustainment (E-BOSS) Program. Learn More: www.galois.com/project/brac...

“Galois is a Goldilocks place between academia and a giant tech company,” says Galois Principal Scientist Katrina Schleisman. “You can do work that is important to you, generate innovative ideas, and make an impact in the broader world.” Learn more: www.youtube.com/watch?v=Jpur...

The world is awash with electronic devices equipped with microphones and capable of recording speech. Add in biometric recognition, emotional screening, and similar audio analysis technology, and you have a context in which it has become very difficult to speak anonymously.

c2rust is available on the Godbolt Compiler Explorer! c2rust is a tool we developed with Immunant that can convert nearly any piece of C code into compilable Rust godbolt.org/z/crsWEGEKM

Galois has released new versions of our core verification tools: SAW 1.3, Cryptol 3.3.0, and Crux 0.10. These updates reflect a new push to make these tools more accessible and user-friendly. Learn more in our latest article: www.galois.com/articles/gal...

Introducing GREASE: Our open-source tool for uncovering hidden vulnerabilities in binary code. Learn more in our latest: www.galois.com/articles/int...

Great writeup from @tweedegolf.bsky.social about their experience using Galois and Immunant's c2rust tool to translate bzip2 from C code to a Rust implementation. Give it a read! tweedegolf.nl/en/blog/151/...

Galois, GE Aerospace, and the University of Vermont (UVM) are excited to announce a collaboration on the Anonymous Real-Time Speech (ARTS) program, which seeks to develop new technologies for anonymizing conversational speech to help safeguard individual speakers’ identities.

In a recent (excellent) WSJ 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! www.wsj.com/articles/why...

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. www.youtube.com/watch?v=q5Ov...

Galois Awarded $12.6M by DARPA to support COOP Program. Learn more: www.galois.com/articles/gal...

OpenAI recently announced their new model, o3. Most media attention focused on its impressive results on the ARC-AGI benchmark, but for us at Galois, the most significant result was the model’s 25% score on a benchmark called Frontier Math. Learn more: www.galois.com/articles/o3-...