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 on DARPA’s PEARLS Artificial Intelligence […]

In May 2016, the newly created Decentralized Autonomous Organization (DAO), an investor-directed venture capital fund built as a smart contract on the Ethereum blockchain, raised around $150 million worth of digital currency. Hopes were high. The fund was to be a fully transparent and decentralized organization, with investment decisions made collectively through member votes, and […]

“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 […]

Among the many tales of innovation and impact to come from Galois over the years, the origin story of Cryptol and SAW is perhaps the most closely tied with that of the company itself. Today, these open-source verification tools have been used in national security, fintech, and cloud computing applications to keep citizens, systems, and […]

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 […]

While most engineers and scientists join Galois to be part of a company that conducts groundbreaking research, for our unique culture of collaboration, or for the great benefits and work-life balance, there’s a lesser-known but equally exciting perk of working at Galois: participating in the creation of spinouts.  Throughout my time as a research engineer […]

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 […]

Thus far in our ongoing series on artificial intelligence we’ve spoken in depth on questions of trust, human perception, and limitations of generative models. We have focused specifically on large language models (LLMs), due in part to their recent successes and media attention. We’ve explored questions of data, testing, and broad model implications. However, LLMs […]

In this post, we describe a new memory model that we have added to our Macaw binary analysis framework which dramatically improves its performance when dealing with large binaries. Galois continues to invest in our binary analysis tools because they address a significant problem: many developers distribute closed source binaries that cannot be analyzed with […]

Galois has long been an advocate of utilizing formal approaches, such as mathematics, models, data, artificial intelligence and more, to build better systems. Galois had the privilege to continue this advocacy by supporting the Dayton Digital Transformation Summit, which took place from August 2 – 4, 2022, in partnership with the Air Force Digital Transformation […]