What does long-term success look like for a verification tool like SAW? For us, it involves improving the quality, correctness, and security of as much code as possible. We know that the best way to get there is not Galois hoarding all of the proofs and proof skills and keeping you all out. We love […]

At Galois, we’ve run into NCC’s Cryptography Group numerous times, because Galois’ services and NCC’s complement each other extremely well. For example in the ‘blst’ cryptographic library project from Supranational, Ethereum Foundation, and Protocol Labs, NCC provided a public audit and report, while we at Galois have verified much of the core library. When I […]

2020 was certainly an interesting year. Amidst a global pandemic and major societal issues,  keeping software and hardware systems trustworthy continued to be challenging. From election systems to ransomware to privacy breaches and online banking theft, the challenges of trustworthy software are alive and well. In this arena, Galois and our partners advanced the state […]

In his 1900 book The Wonderful Wizard of Oz, L. Frank Baum tells a story that will resonate with any software engineer. A woodman by the name of Nick Chopper suffers a series of workplace accidents. In turn, his arms, legs, body, and even his head are replaced by metal prosthetics. Eventually, what remains is […]

Galois is innovating ways to create accessible data models or make existing data models actionable during a crisis like COVID 19. I blogged about this in April and, more specifically, in October when I wrote about our AMIDOL project.  This month, I wanted to talk about our exciting work with SuperMaaS – a modeling-as-a-service (MaaS) […]

In the film Rocky Balboa, Rocky tells his son, “Nobody is gonna hit as hard as life. But it ain’t how hard you hit; it’s about how hard you can get hit and keep moving forward.”   At Galois, we appreciate Rocky’s tenacity and inventiveness. Rocky is the ultimate underdog who perseveres despite overwhelming odds. We […]

Shpat Morina and I are happy to introduce the new Galois podcast, Building Better Systems. We put this podcast together to provide us an opportunity to have deep, directed discussions with anyone who wants to build better systems. We’re approaching the challenge from two sides. We want to know what challenges people face today and […]

This blog is the second in a series of posts about a joint project between Galois, Supranational, The Ethereum Foundation, and Protocol labs verifying the blst signature library. You can find the first post here. It’s a combination of my bad jokes and an overview of what we’re trying to achieve.  It’s happening already. The […]

The standard development tools for the Rust language provide a convenient mechanism for embedding tests within your code that can then be automatically run using the `cargo test` command. This video shows how to migrate from testing to verification of Rust programs by converting a standard Rust test to use Galois’ Crux tool. Crux can […]

We are happy to announce the first formal release of Crux, a new open-source verification tool from Galois. This new tool aims to improve software assurance using symbolic testing, a technique that allows for smooth migration from testing to verification. Crux builds on the same infrastructure as our Software Analysis Workbench (SAW), but with a […]