We take pride in personally connecting with all interested partners, collaborators and potential clients. Please email us with a brief description of how you would like to be connected with Galois and we will do our best to respond within one business day.
When an engineer or organization first becomes interested in formal methods, they typically have two big questions: “What are formal methods?” And “Where do I put them?”
We created a whole webpage dedicated to answering the question “What are formal methods?”
The answer to the question, “Where do I put the formal methods?” depends on your goals and starting point.
The short answer is: Prioritize using formal methods on the most critical components of your system - those for which failure would be disastrous. The trick here is figuring out exactly which components of your system need to be prioritized.
Sometimes you already know exactly which component(s) are most critical (for example, a flight controller on a commercial aircraft). In these cases, formal methods can be used to verify the correctness of these components, then compartmentalize and secure them as needed (more on this shortly).
More often, you are either building a system from scratch or have a pre-existing/legacy system for which you want to guarantee correctness and security. When it comes to building a system from scratch, formal methods techniques can be used to create a “correct by construction” and “secure by design” system, designed, specified, and implemented with mathematical guarantees of correctness and security from the start.
Verifying correctness and improving security of existing systems is more complicated, because often the detailed specifications and models on which formal methods depend simply don’t exist. Fortunately, formal methods can help.
In these cases, static and dynamic analysis tools and techniques can be used to create detailed digital models - semi-automatically from codebases or even binary. These serve as mathematically precise system maps you can use to analyze, experiment, optimize, test changes with full understanding of impact; identify, verify, and compartmentalize critical components; and sometimes even automatically generate correct and secure code and hardware designs.
System modeling and analysis often serves as a foundation for next steps. Now that you have used one kind of formal method to objectively achieve better understanding of your system, you can begin to apply other formal methods to targeted critical areas of your system and/or software development lifecycle:
Problem: Testing only covers known cases. Subtle errors still sneak into production, creating costly rework and risk.
Solution: Using formal methods here means automatic static analysis proofs running as part of every build. On each commit, formal proofs check that the code behaves exactly as specified, preventing defects before they land.
.png)
Result/ROI: Fewer defects, faster releases. Embedding formal checks in CI/CD prevents costly late-stage defects and provides evidence of continuous correctness. Teams spend less time chasing bugs and more time delivering features.
Example: With AWS, Galois integrated our Software Analysis Workbench (SAW) into the CI pipeline for their main cryptographic library, s2n-tls. Each change automatically triggers a proof that confirms cryptographic correctness—blocking any insecure code from merging.
Problem: Cyber-physical systems are often so complex that fully understanding the impact of change is nearly impossible. Small design or software update errors lead to overspend, security risks, and project failures.
Solution: Using formal methods here means using static and dynamic analysis tools and techniques to create detailed digital models. These serve as mathematically precise system maps you can use to analyze, experiment, optimize, test changes with full understanding of impact, and even automatically generate correct and secure code and hardware designs.
Result/ROI: Faster, Safer, Cheaper. Virtual experimentation and testing is often dramatically faster and cheaper than building physical prototypes. Teams iterate quickly, uncover issues early, and validate correctness and safety before implementation. Much of formal methods involves identifying and prioritizing the most critical components of your system. System modeling and analysis often serves as a foundation for next steps, including verifying and securing critical components.
Examples: With the 21st Century Cryptography (21CC) project, Galois created the world’s first ever formally verified, side channel resistant, cryptographic microchip. We also tested this approach on a SuperVolo UAV - quickly swapping out a component with full understanding of the impact of that change on safety and performance.
Problem: Malicious or malformed inputs can slip past conventional parsers and compromise systems.
Solution: Using formal methods here means verified parsers, automatically generated from precise specifications and “wrapped” around your system. They act as a gate: no data enters until proven safe.
Result/ROI: More secure, faster certification. Verified parsers eliminate entire classes of injection and memory-safety vulnerabilities at the system perimeter, accelerating certification and reducing time spent on fuzzing, manual testing, and reactive patching.
Example: In DARPA’s HACMS Program, Galois used this approach to “hack-proof” UAVs with provably memory-safe parsers that isolated critical subsystems. In the SafeDocs project, Galois developed parser technologies that are safe by design, and now is creating a pre-qualified parser generator that will automatically generate code that is guaranteed to be secure.
Problem: Legacy software, often written in C, C++, or even just assembly code, is the foundation of many of our most critical systems. Virtually all of these systems struggle to meet today's higher standards for security, speed, and performance. As a result, the Department of Defense has a critical need to be able to modify, update, and maintain legacy software.
Solution: Using formal methods here means using tools to lift models from a legacy codebase, use those models to automate analysis, modify or upgrade discrete blocks of code using these models, and easily slot the modified code back into the legacy system for higher security or improved performance.
Result/ROI: Lower cost, safer upgrades, incremental modernization. Rather than rewrite entire systems, you can upgrade critical components safely, preserve compatibility, and reduce technical debt over time. This lowers total lifecycle cost, increases maintainability, and brings legacy systems up to modern security and performance standards without disrupting operations.
Examples: In the Polymorph project, Galois developed a cohesive tool chain to do exactly this. Equipped with these tools, users can treat legacy codebases as modular systems - upgrading them incrementally over time, all while benefiting from greater understanding of their codebases and the peace of mind that comes from continuous, provable correctness. Galois also developed C2Rust, our automatic migration tool that is able to translate most C modules into semantically equivalent Rust code.
Problem: Blockchains are unforgiving: once deployed, smart contracts transactions can’t be rolled back without forking the chain, and any vulnerability becomes an immediate target for exploitation. Conventional audits and testing often miss subtle logic errors and edge cases that lead to significant financial losses and damaged trust.
Solution: Using formal methods here means using verification tools to specify exactly how a smart contract or protocol must behave—and using machine-checked proofs to guarantee it does. This approach uncovers hidden bugs early, verifies critical properties (like correctness and safety), and ensures deployed code matches your intent. It can also mean verifying zero knowledge (ZK) circuits and verifier backends to verify that transactions are correct, improving efficiency and scalability while maintaining privacy and security.
Result/ROI: Reduced risk, trust at scale. Verified contracts and protocols dramatically reduce the risk of catastrophic exploits and financial loss. They help you prove due diligence to regulators, reassure investors, and differentiate your platform as safe and robust in a crowded market.
Examples: Galois has conducted formal verification and analysis for several blockchain companies:
Portland, OR
421 SW 6th Avenue, Suite 300
Portland, Oregon 97204
Arlington, VA
901 N Stuart Street, Suite 501
Arlington, Virginia 22203
© Copyright Galois, Inc. 2024. All Rights Reserved | Terms of Use | Privacy Policy
