Lightnews — Scholar-powered news

Galois @galoisinc.bsky.social · 3d

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...

Galois @galoisinc.bsky.social · 5d

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...

Towards a verified Jolt zkVM

www.galois.com

1 1

Galois @galoisinc.bsky.social · 12d

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...

2

Galois @galoisinc.bsky.social · 18d

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...

Galois Internship Round 2: A Second Summer Intern Experience

www.galois.com

Galois @galoisinc.bsky.social · 23d

Starting from the beginning? Check out our "What are Formal Methods?" explainer here: www.galois.com/what-are-for...

What Are Formal Methods? | Galois

Think of formal methods as a mathematical safety net for critical systems. They use logic-based reasoning to prove that a system always behaves correctly.

www.galois.com

Galois @galoisinc.bsky.social · 23d

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...

1

Galois @galoisinc.bsky.social · 25d

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...

1 1

Galois @galoisinc.bsky.social · Sep 11

"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...

1

Galois @galoisinc.bsky.social · Sep 2

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 @galoisinc.bsky.social · Aug 25

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!

Galois @galoisinc.bsky.social · Aug 18

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...

1 3

Galois @galoisinc.bsky.social · Aug 14

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 Releases Dioptra: An analytic tool for OpenFHE programs

www.galois.com

Galois @galoisinc.bsky.social · Aug 7

"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...

Building the Future, Securely: Reflections on My Summer at Galois

www.galois.com

Galois @galoisinc.bsky.social · Jul 24

Learn more about our work with the Census Bureau and Differential Privacy here: www.galois.com/project/census

Galois - Census

www.galois.com

Galois @galoisinc.bsky.social · Jul 24

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...

A Simulated Reconstruction and Reidentification Attack on the 2010 U.S. Census

Forthcoming. Now Available: Just Accepted Version.

hdsr.mitpress.mit.edu

1 1

Galois @galoisinc.bsky.social · Jul 22

🚨 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/...

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

1

Galois @galoisinc.bsky.social · Jul 15

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

Specifications Don't Exist

www.galois.com

3

Galois @galoisinc.bsky.social · Jun 26

“[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?...

Closing: HON. Emil Michael, Under Secretary of Defense for Research and Engineering

YouTube video by DARPAtv

youtu.be

Galois @galoisinc.bsky.social · Jun 17

🎉 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!

1

Galois @galoisinc.bsky.social · Jun 4

In our latest article, Ariel writes about the work that, in part, led to this award - and how rigorous verification techniques can unlock greater confidence and correctness in large-scale simulations, from climate models to public health interventions and beyond.

www.galois.com/articles/for...

Galois @galoisinc.bsky.social · Jun 4

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!

1

Galois @galoisinc.bsky.social · May 27

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...

A labyrinth icon, serving as a metaphor for the process of formal verification

2 1

Galois @galoisinc.bsky.social · May 22

If you're an experienced, curiosity-driven researcher and technical leader at the intersection of Formal Methods and AI/ML, Digital Engineering, or Cryptography, we'd love to hear from you!

apply.workable.com/galois/j/4A9...

Principal Scientist - Galois

About GaloisGalois tackles the hardest problems in computer science. Our mission is to assure trust in critical systems that protect the privacy and integrity of information in the real world. Core to...

apply.workable.com

Galois @galoisinc.bsky.social · May 22

"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.

1

Galois @galoisinc.bsky.social · May 13

Want your research to make a global impact? Galois is hiring Principal Scientists in all four of our locations. Join us: www.galois.com/careers#open...

Galois - Careers

www.galois.com