Galois
@galoisinc.bsky.social
galois.com
For nearly 25 years, Galois has combined mathematical rigor with curious creativity to cut through complexity and guarantee trustworthiness in the world’s most critical systems.
For nearly 25 years, Galois has combined mathematical rigor with curious creativity to cut through complexity and guarantee trustworthiness in the world’s most critical systems.
Galois has released updated versions of our Software Analysis Workbench (SAW) and Cryptol, including a wide variety of new features, bugfixes, and enhancements.
Learn more: www.galois.com/articles/gal...
Learn more: www.galois.com/articles/gal...
November 26, 2025 at 4:24 PM
Galois has released updated versions of our Software Analysis Workbench (SAW) and Cryptol, including a wide variety of new features, bugfixes, and enhancements.
Learn more: www.galois.com/articles/gal...
Learn more: www.galois.com/articles/gal...
Congrats to Galois spinout Free & Fair, which last week released VoteSecure, a new cryptographic protocol and SDK supporting end-to-end verifiable remote/internet voting. This great example of Rigorous Digital Engineering in action has been featured in several news outlets.
November 17, 2025 at 5:18 PM
Congrats to Galois spinout Free & Fair, which last week released VoteSecure, a new cryptographic protocol and SDK supporting end-to-end verifiable remote/internet voting. This great example of Rigorous Digital Engineering in action has been featured in several news outlets.
At Galois, 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're so glad you asked. Learn more here: www.galois.com/what-are-for...
But what exactly are formal methods? How do they work, and why are they so important?
We're so glad you asked. Learn more here: www.galois.com/what-are-for...
November 13, 2025 at 5:40 PM
At Galois, 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're so glad you asked. Learn more here: www.galois.com/what-are-for...
But what exactly are formal methods? How do they work, and why are they so important?
We're so glad you asked. Learn more here: www.galois.com/what-are-for...
Last month, Galois Principal Scientist @m-dodds.bsky.social wrote an article about his work exploring using Claude for interactive theorem proving (www.galois.com/articles/cla...).
His experiments have continued, with some fun results!
His experiments have continued, with some fun results!
October 29, 2025 at 10:07 PM
Last month, Galois Principal Scientist @m-dodds.bsky.social wrote an article about his work exploring using Claude for interactive theorem proving (www.galois.com/articles/cla...).
His experiments have continued, with some fun results!
His experiments have continued, with some fun results!
Galois Research Engineer Sourya Dey’s paper “Token embeddings violate the manifold hypothesis” has been accepted to NeurIPS 2025!
Come see Dey, with co-authors Michael Robinson and Tony Chiang, in San Diego this December, or dive into the paper here: arxiv.org/abs/2504.01002
Come see Dey, with co-authors Michael Robinson and Tony Chiang, in San Diego this December, or dive into the paper here: arxiv.org/abs/2504.01002
Token embeddings violate the manifold hypothesis
A full understanding of the behavior of a large language model (LLM) requires our grasp of its input token space. If this space differs from our assumptions, our comprehension of and conclusions about...
arxiv.org
October 27, 2025 at 7:43 PM
Galois Research Engineer Sourya Dey’s paper “Token embeddings violate the manifold hypothesis” has been accepted to NeurIPS 2025!
Come see Dey, with co-authors Michael Robinson and Tony Chiang, in San Diego this December, or dive into the paper here: arxiv.org/abs/2504.01002
Come see Dey, with co-authors Michael Robinson and Tony Chiang, in San Diego this December, or dive into the paper here: arxiv.org/abs/2504.01002
@aria-research.bsky.social has awarded seed funding to Galois for FV-Spec – a new large-scale benchmark of real-world challenge problems to measure and accelerate AI capabilities in formally verifying software.
Learn more: www.aria.org.uk/opportunity-...
Learn more: www.aria.org.uk/opportunity-...
Mathematics for Safe AI
We don’t yet have known technical solutions to ensure that powerful AI systems interact as intended with real-world systems and populations. A combination of scientific world-models and mathematical p...
www.aria.org.uk
October 24, 2025 at 3:27 PM
@aria-research.bsky.social has awarded seed funding to Galois for FV-Spec – a new large-scale benchmark of real-world challenge problems to measure and accelerate AI capabilities in formally verifying software.
Learn more: www.aria.org.uk/opportunity-...
Learn more: www.aria.org.uk/opportunity-...
For chipmakers, design-hiding is a $100B problem.
Most outsource fab to untrusted foundries—but foundries can fabricate a chip from encrypted designs.
In our latest, Tom Shrimpton defines the problem, explores potential solutions, and looks ahead.
🔗 www.galois.com/articles/rev...
Most outsource fab to untrusted foundries—but foundries can fabricate a chip from encrypted designs.
In our latest, Tom Shrimpton defines the problem, explores potential solutions, and looks ahead.
🔗 www.galois.com/articles/rev...
Reverse Engineer THIS! Towards Provable Cryptographic Protection for Circuit IP
www.galois.com
October 13, 2025 at 8:40 PM
For chipmakers, design-hiding is a $100B problem.
Most outsource fab to untrusted foundries—but foundries can fabricate a chip from encrypted designs.
In our latest, Tom Shrimpton defines the problem, explores potential solutions, and looks ahead.
🔗 www.galois.com/articles/rev...
Most outsource fab to untrusted foundries—but foundries can fabricate a chip from encrypted designs.
In our latest, Tom Shrimpton defines the problem, explores potential solutions, and looks ahead.
🔗 www.galois.com/articles/rev...
With GAI4RDE, Galois developed RDE Wingman: an LLM-based, multi-agent framework that automates RDE workflows.
“In a single day, using RDE Wingman could save me 2 weeks of work,” said Galois Principal Scientist Joe Kiniry. “It’s making RDE 10 to 100X faster.”
www.galois.com/articles/gen...
“In a single day, using RDE Wingman could save me 2 weeks of work,” said Galois Principal Scientist Joe Kiniry. “It’s making RDE 10 to 100X faster.”
www.galois.com/articles/gen...
October 8, 2025 at 4:58 PM
With GAI4RDE, Galois developed RDE Wingman: an LLM-based, multi-agent framework that automates RDE workflows.
“In a single day, using RDE Wingman could save me 2 weeks of work,” said Galois Principal Scientist Joe Kiniry. “It’s making RDE 10 to 100X faster.”
www.galois.com/articles/gen...
“In a single day, using RDE Wingman could save me 2 weeks of work,” said Galois Principal Scientist Joe Kiniry. “It’s making RDE 10 to 100X faster.”
www.galois.com/articles/gen...
We’re excited to kick off stage 2 of our project to verify the Jolt zkVM! Thank you to the Ethereum Foundation Ecosystem Support Program for the grant to fund this effort.
Check out our post from January to learn more about the project: www.galois.com/articles/tow...
Check out our post from January to learn more about the project: www.galois.com/articles/tow...
Towards a verified Jolt zkVM
www.galois.com
October 6, 2025 at 5:05 PM
We’re excited to kick off stage 2 of our project to verify the Jolt zkVM! Thank you to the Ethereum Foundation Ecosystem Support Program for the grant to fund this effort.
Check out our post from January to learn more about the project: www.galois.com/articles/tow...
Check out our post from January to learn more about the project: www.galois.com/articles/tow...
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...
Learn more:
www.galois.com/articles/aut...
September 29, 2025 at 8:26 PM
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...
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...
Read more: www.galois.com/articles/gal...
Galois Internship Round 2: A Second Summer Intern Experience
www.galois.com
September 23, 2025 at 4:50 PM
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...
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...
Our latest explainer digs in: www.galois.com/where-do-i-p...
September 18, 2025 at 6:57 PM
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...
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...
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...
September 16, 2025 at 4:34 PM
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...
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...
Read more in our Q&A with Angel: www.galois.com/articles/gal...
September 11, 2025 at 4:30 PM
"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...
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...
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...
September 2, 2025 at 5:29 PM
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...
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!
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!
August 25, 2025 at 4:13 PM
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!
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...
Learn more: galois.com/articles/esc...
August 18, 2025 at 5:09 PM
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...
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...
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 Releases Dioptra: An analytic tool for OpenFHE programs
www.galois.com
August 14, 2025 at 5:58 PM
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...
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...
Read more: www.galois.com/articles/ref...
Building the Future, Securely: Reflections on My Summer at Galois
www.galois.com
August 7, 2025 at 4:33 PM
"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...
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...
Read more:
hdsr.mitpress.mit.edu/pub/ntchx9im...
A Simulated Reconstruction and Reidentification Attack on the 2010 U.S. Census
Forthcoming. Now Available: Just Accepted Version.
hdsr.mitpress.mit.edu
July 24, 2025 at 7:18 PM
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...
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/...
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/...
Cheesecloth: Zero-Knowledge Proofs of Real-World Vulnerabilities | ACM Transactions on Privacy and Security
Currently, when a security analyst discovers a vulnerability in critical software
system, they must navigate a fraught dilemma: immediately disclosing the vulnerability
to the public could harm the sy...
dl.acm.org
July 22, 2025 at 8:45 PM
🚨 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/...
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
Give it a read!
www.galois.com/articles/specifications-dont-exist
Specifications Don't Exist
www.galois.com
July 15, 2025 at 7:04 PM
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
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?...
- HON. Emil Michal, Undersecretary of Defense for Research and Engineering
youtu.be/ROZv0G-6zxs?...
Closing: HON. Emil Michael, Under Secretary of Defense for Research and Engineering
YouTube video by DARPAtv
youtu.be
June 26, 2025 at 5:41 PM
“[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?...
- 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!
If you’re at PLDI, swing by to say “Hi,” chat about Galois, and nerd out on automata & #NetKAT for packet-switched networks!
June 17, 2025 at 5:37 PM
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!
June 4, 2025 at 8:04 PM
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!