Overview
Galois is an engineering firm that proves software does what it is supposed to do. The technique is called formal methods, and it works the way a mathematical proof does: reason about a program once, and the conclusion holds for every possible input, not just the handful of cases a test happens to try1. Organizations hire Galois for systems where a bug is unacceptable, among them NASA, DARPA and Amazon2.
On Cardano, Galois architected the Network Service Assurance tool for Input Output, which samples latency statistics across multiple nodes to produce status updates and flag attacks or performance degradation; the firm also wrote networking and ledger code for the chain3. On Midnight, Galois worked with the Midnight team and Intersect to add recursion to Halo2, an open-source library for zero-knowledge proofs, which show that a statement is true without revealing the data behind it4. Intersect separately lists Galois among contributors to the repositories holding Cardano's formal specifications and consensus code5.
Key Features
- Verification tools anyone can download. Cryptol is a language for specifying what a cryptographic algorithm should do, and SAW checks properties of code written in C, Java, Rust or Cryptol against such a specification6.
- Cardano network monitoring you can run yourself. The Network Service Assurance code is published as Haskell under the Apache 2.0 license, with documentation covering installation and how to stand it up inside the Cardano network7.
- One proof that stands in for a chain's whole history. Recursion lets proofs nest, so verifying the proof on one block also verifies the proofs on all previous blocks, and a checker no longer walks the chain transaction by transaction4.
- Contracts get the same treatment as protocol code. Working with the Stellar Foundation, Galois built Formal Verso to check smart contracts, the programs that run directly on a blockchain3. The tool is a Rust front end on the firm's Software Analysis Workbench8.
What to Expect
Galois sells services rather than a product, so there is nothing to sign up for and no pricing page. The contact panel on the site asks for a short description of how you would like to be connected with the firm, and gives an email address and a phone number2.
What the site offers instead is reading material. Project pages describe individual engagements and name the organizations behind them, and a plain-English explainer walks through formal methods for readers who have never met the term, including worked examples1. The blockchain page collects the chain work in one place, because it names each engagement and the partner it was done with3.
Developers will get more out of the GitHub organization, which hosts the verification tooling and the Cardano monitoring code in public9. The tools index is a better starting point than the repository list, because each entry says in one line what the tool is for before sending you to its documentation6.
Galois is fully employee-owned, and splits its work between funded research on one side and applied delivery for clients on the other2.
