2025 Year in Review

As 2025 comes to a close, we’re proud to reflect on a year at Galois defined by innovation, rigor, and real-world impact. From new verification and analysis tools to formal methods science communications, 2025 was a year of connecting deep technical foundations with practical application.

Highlights

New Tools: Galois released several significant tools aimed at uncovering subtle, high-impact vulnerabilities in real systems. GREASE, an open-source, under-constrained symbolic execution tool, helps engineers uncover hidden vulnerabilities in binary code. Dioptra, an analytic tool, helps developers navigate the complex tradeoff space (between speed, security, memory usage, and capability fit) of fully homomorphic encryption (FHE) programs. 

Cryptographic Innovation: Our cryptography and privacy research continued to push towards performance under real-world constraints—achieving meaningful security without sacrificing practicality. From formally verifying zero-knowledge proofs for blockchain applications to verifiable computation under DARPA’s COOP program, Galois continues to lead the way at the intersection of cryptographic rigor and deployable systems. 

AI + Formal Methods: With the Generative Artificial Intelligence for Rigorous Digital Engineering (GAI4RDE) Project, Galois developed Galwagent, an LLM-based, multi-agent framework that automates RDE workflows. Others across Galois explored the intersection of AI and formal methods, including experimenting with using Claude Code for interactive theorem proving. 

Making Formal Methods Understandable: We released a series of scrollytelling explainer pages – including What Are Formal Methods? and Where Do I Put the Formal Methods? – designed to help engineers, program managers, and decision-makers understand how these rigorous mathematical techniques fit into real software and system applications and lifecycles.  These resources reflect our broader push to move formal methods from specialist tooling to everyday engineering conversations.

Software/Tool Releases, Updates, and Commercialization

Galois released Cryptol 3.4.0, Crux 0.11, and SAW 1.4 – significant updates to our core set of formal verification tools.

We released GREASE, an under-constrained symbolic execution tool for finding bugs in and checking properties of binaries and LLVM bitcode, designed to surface vulnerabilities that evade traditional analysis. 

We also released Dioptra, an analytic tool for OpenFHE programs. 

Software and Systems Analysis (SSA)

Santiago Cuéllar, Naomi Spargo, Jonathan Daugherty, and David Darais presented “Designing Walrus: Relational Programming with Rich Types, On-Demand Laziness, and Structured Traces” at miniKanren’25. 

That same authorial team, joined by Chris Phifer, also presented “The CoCompiler: DSL Lifting via Relational Compilation" at the same conference. The paper explores CoCompiler, a bidirectional compiler and lifter between C and Lustre, showing how writing a compiler as a relation, rather than as a traditional function, yields a DSL lifter “for free.”

Galwegian Naomi Spargo, along with co-authors Nikolaus Huber, Nicolas Osborne, Samuel Hym, and Jan Midtgaard, presented “Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM” at TACAS 2025.

In addition, we published “scrollytelling” web pages addressing common questions about Galois’s bread and butter – formal methods. What Are Formal Methods? and Where Do I Put the Formal Methods? were created to complement our research output by serving as a resource for non-specialists to help them understand how rigorous mathematical techniques integrate into modern engineering workflows and solve real world problems. 

Additional Thought Leadership & Blogs

• Claude Can (Sometimes) Prove It – Mike Dodds
• Specifications Don’t Exist – Mike Dodds
• What Works (and Doesn’t) Selling Formal Methods by Mike Dodds
• Introducing GREASE: An Open-Source Tool for Uncovering Hidden Vulnerabilities in Binary Code by Langston Barrett, Ryan Scott, Ben Davis, and Matt Bauer
• Formal Methods and Scientific Computing – Ariel Kellison
• Automated Lean Proofs for Every Type – Elizaveta Pertseva

Advanced Cryptography and Privacy 

David Holland gave a talk at the 2025 New England Systems Verification Day about Formal Verso, which leverages formal verification to eliminate vulnerabilities in Rust-based smart contracts. 

Galwegians Santiago Cuéllar Gempeler, James Parker, and Stuart Pernsteiner, along with co-authors Bill Harris, Ian Sweet and Eran Tromer, published “Cheesecloth: Zero Knowledge Proofs of Real-World Vulnerabilities” in ACM Transactions on Privacy and Security, Volume 28. 

James Parker gave a talk entitled Towards a verified Jolt zkVM at ZKProof 7 in Sofia, Bulgaria. 

Galwegians David Darais, Sourya Dey, and Scott Moore, with numerous co-authors, published a “A Simulated Reconstruction and Reidentification Attack on the 2010 U.S. Census” in the Harvard Data Science Review, demonstrating how individual, confidential records could reconstructed from the published census summaries. 

Additional Thought Leadership and Blogs

• Reverse Engineer THIS! Towards Provable Cryptographic Protection for Circuit IP – Tom Shrimpton
• VOXLET: Pioneering Private Voice-Changing Technology – Andrew Shaughnessy
• Galois Awarded $12.6M by DARPA to support COOP Program
• Towards a Verified Jolt zkVM – James Parker

Rigorous Digital Engineering (RDE) 

With the Generative Artificial Intelligence for Rigorous Digital Engineering (GAI4RDE) Project, Galois developed Galwagent, an LLM-based, multi-agent framework that automates RDE workflows. 

Galois published a “scrollytelling” explainer on updating legacy systems with Polymorph, exploring how RDE tools and techniques support real-world system modernization. Tools and methodologies from Polymorph are actively being transitioned to program offices across the DoD.

‍Additional Thought Leadership and Blogs

• Generative AI for Rigorous Digital Engineering – Andrew Shaughnessy
• Escaping Isla Nublar: Coming around to LLMs for Formal Methods – Twain Byrnes

AI/ML and Data Science

Katrina Schleisman was invited to an in-person roundtable on complexity science at DARPA DSO in September 2025. She also gave an invited talk, “Modeling the Complexity of Memory in AI Systems” for the DSO Speaker Series on Complex, Dynamic, and Adaptive Systems in November 2025.

Galwegians Sourya Dey and Taisa Kushner, along with co-author Michael Robinson, published “Probing the Topology of the Space of Tokens with Structured Prompts” in a special issue of Mathematics focused on new perspectives in harmonic analysis. In the paper, the authors propose a method to prompt LLMs to reveal their token embeddings, leading to increased transparency of GenAI systems.  

Galwegian Sourya Dey, along with co-authors Michael Robinson and Tony Chiang, presented “Token Embeddings Violate the Manifold Hypothesis” at NeurIPS 2025 in San Diego, California, proposing a method to identify unstable tokens in LLMs and potential implications for model behavior. 

Dey also presented a poster on “Investigating Knowledge Closure of Large Language Models via Token Embeddings” at the NSF Workshop on the Science of Safe AI, and served as a reviewer for the 2025 Asian Conference on Machine Learning (ACML) and Transactions on Machine Learning Research (TMLR). 

Additional Thought Leadership and Blogs

• Privacy vs. Power: Can LLMs Succeed in Security-Critical Environments? – Kevin Fisher
• O3, Frontier Math, and the Future of Mathematics – Mike Dodds

Miscellaneous Blogs and Publications

• Galois Internship Round 2: A Second Summer Intern Experience – Mark Moeller
• Galois Intern Q&A: Angel Gallegos 
• Building the Future, Securely: Reflections on My Summer at Galois – Mariana Ferreira

Community Involvement: Committees, Boards, Panels, Seminars, and Workshops

Tyler Smith spoke as a panelist at NVIDIA Formal Methods Week.

Taisa Kushner was a featured panelist on “AI-Driven Digital Twins for Aerospace, Defense, & Healthcare” at the Dayton Digital Transformation Summit. 

Ryan Scott served on the program committee for FUNARCH 2025.

Scott Moore served on the program committees for CSF 2025 & 2026, LangSec 2025, USENIX Security 2025 & 2026, and PLDI 2026.

Joe Kiniry served on several program committees and editorial boards, including FM 2026 Industry Day, iFM 2025, NFM 2025, the IEEE Security & Privacy's Award Committee for the IEEE Cybersecurity Award for Practice, and the Cambridge University Press journal, Research Directions: Cyber-Physical Systems.

Galois sponsored the 2025 Midwest Programming Languages Summit, with numerous Galwegians in attendance.

Looking Forward

As critical systems grow more complex, and as AI grows more capable, the need for correctness, security, and reliability has never been greater. We’re excited to continue spearheading research, building tools, and developing formal-methods-driven solutions to the world’s thorniest problems. Thank you to our collaborators and the Galwegian community for pushing this important work forward with curiosity, care, and technical excellence.