Formal methods (Galois’s bread and butter) are a suite of mathematically-based techniques for specifying, developing, and verifying software and hardware systems, providing an unparalleled degree of assurance in system correctness and security. These techniques are extraordinarily valuable, but can be prohibitively time-consuming, laborious, and expensive for all but the most critical systems for which failure is not an option.
Galois is actively working on developing interactive tools that harness the potential of generative AI technologies to make formal methods more accessible to and usable by a wider base of people. Already, novel generative AI technologies have emerged that can assist with implementation and verification. Our research focuses on crafting AI tools that can assist with generating accurate, detailed, and robust system specifications. By integrating AI assistance into the DevSecOps pipeline, we aim to reduce the cognitive load and manual efforts of engineers, speeding up the design process, enhancing quality control, and cutting down overall costs.
With our combined expertise in AI and Formal Methods, Galois is paving the way for a new era in formal methods, where artificial intelligence empowers humans to build more secure, reliable, and effective systems with unprecedented efficiency.