A software proof can be correct on Monday and obsolete by Friday. Somebody changes a data structure, optimizes a loop, or adds a feature. The program moves on. The beautiful mathematical argument stays behind. For a company selling confidence in code, this is an awkward little problem: how do you keep confidence from expiring?
- Galois builds tools and research for checking critical software and hardware.
- Cryptol writes the specification; SAW helps check whether code follows it.
- AWS and Apple show how the tools fit into production engineering.
Galois, a Portland computer science research company, has spent years working on that gap. Its customers include NASA, DARPA, Amazon and the Department of Defense. These organizations have different missions, but share an uncomfortable dependency: important promises eventually become instructions running on machines.
01 / A professor’s hesitation
The company began in 1999 with John Launchbury, then a professor at the Oregon Graduate Institute. Work modeling a cryptographic chip for the National Security Agency led to a request: could he build a language for describing cryptographic algorithms?
He hesitated. Academic research rewarded publishable discoveries; a useful product needed sustained engineering. Launchbury thought trying to satisfy both could compromise each. Forming a company offered another route. Galois’s first government contract produced Cryptol, a language that made cryptographic specifications executable.
That distinction matters. An algorithm in a paper and an implementation in code can look very different. Somewhere between the mathematics and the machine, a programmer must make hundreds of small decisions. Cryptol gives engineers a precise model against which those decisions can be checked.
02 / Make the promise executable
Consider an encryption routine. Testing feeds it chosen examples and checks the answers. Formal verification asks whether specified properties hold across the inputs covered by the proof. A carefully chosen test can expose a mistake. A successful proof can rule out a defined class of mistakes.
Galois’s Software Analysis Workbench, or SAW, connects specifications to implementations. It extracts mathematical models from code and uses automated reasoning tools to check them. Engineers guide the process. When an implementation disagrees with its specification, a counterexample can help explain why.
The appeal is particularly clear in cryptography, where arithmetic is intricate and an obscure corner case can have consequences far beyond its size. SAW’s documentation describes symbolic execution, which reasons about inputs symbolically rather than trying each concrete value. Bounded loops, common in cryptographic routines, suit this approach.
03 / The expensive part comes first
AWS contracted with Galois to make verification of its s2n encryption software more practical. The obstacle was engineering friction. Earlier approaches demanded too much intervention when code changed, or failed to scale. A proof that developers must constantly repair has a difficult time earning a permanent place in their workflow.
The joint 2018 case study records the investment: roughly three months of engineering effort each for HMAC and a deterministic random-bit generator, and eight months for the TLS handshake. Those figures included learning the code, writing specifications, building proofs and integrating checks into development. They describe effort, not a published dollar price.
The payoff appeared afterward. For the HMAC proof discussed in the paper, a year of code changes required only three manual updates. Checks ran when code was pushed or a pull request opened. Verification became a recurring development activity, with much of the specialist work concentrated upfront.
The practical question: can the proof keep up with the programmer?A question at the heart of continuous verification
04 / Apple finds the seams
Apple’s May 2026 account of verifying post-quantum cryptography illustrates another problem: different mathematical descriptions need a reliable connection. Apple used SAW and Cryptol alongside the Isabelle proof assistant. Galois built a translator, specified by Apple, that moved Cryptol models into Isabelle.
Apple reported finding a missing step in an early ML-DSA implementation that could produce incorrect output in rare cases. It also repaired an error in a third-party proof. Checking the checker, it turns out, belongs in the job description.
The account is candid about boundaries. Its approach assumes correct compiler behavior. A SAW limitation prevented verification across every possible ML-DSA message size, so Apple combined proof with conventional testing. Functional correctness also leaves other security questions to address. Reading those qualifications is part of understanding what the result buys.
05 / The researchers own the shop
Galois earns money through sponsored research and commercial engineering, while making tools such as Cryptol and SAW open source. Some technologies move into commercial spinouts. CAMET, its systems modeling library, has a separate offering: free access for up to ten users per organization, with an enterprise option beyond that.
Its organization is unusual, too. Employees, called Galwegians, became the company’s full owners in June 2023 through an employee stock ownership plan introduced a decade earlier. The company describes internally transparent salaries and a Collaborative Web structure without traditional managers. Its annual Blue Sky time gives employees a week for creativity or innovation.
06 / Start with one critical promise
The market position is specific: research and assurance for difficult systems, supported by tools engineers can inspect. Alternatives include internal verification teams and other verified cryptography toolchains. The choice depends on languages, properties and integration needs. Several approaches can coexist in one system.
The work now extends into hospitals. In June 2026, Galois reported that its team, working with Kry10, defended eight of nine vulnerability challenges in an ARPA-H hackathon using simulated hospital networks. September brought HealthyDocs, a research project for securely integrating medical-device and health-record data.
For another engineering team, the transferable move is modest: choose one consequential behavior, describe it precisely, and check it whenever the code changes. Budget for expertise and maintenance. Pick assumptions you can defend. The first useful question is wonderfully plain: what, exactly, are we promising?