GET IN TOUCH
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.
PRAXIS
Challenge
AI is accelerating offensive cyber capabilities faster than conventional defenses can adapt. While techniques like formal verification, translation to memory-safe languages, and safe parser generation eliminate entire categories of software vulnerabilities, they require massive time investments, deep specialized expertise, and painstaking manual effort. For most organizations, the cost quickly becomes prohibitive.
AI models could bridge this gap by automating the most difficult and time-consuming parts of formal verification – making proof engineering dramatically faster, cheaper, and easier for non-experts to use. This AI-driven pipeline could break through the human bottleneck that currently limits formal methods, allowing defensive software assurance to scale alongside AI-driven threats.
However, today’s frontier models are not trained for formal reasoning or verification, and the requisite training data and evaluation infrastructure do not yet exist. Bridging this gap requires formal methods benchmarks designed to train and evaluate AI models on critical defensive tasks: identifying unsafe code, generating formal specifications for legacy systems, and producing verified, secure alternatives.
Solution
With PRAXIS (AKA Formal Methods Benchmarks for AI-Enabled Cyber Defense), Galois and RAND are developing formal methods benchmarks to train and evaluate AI models on critical cybersecurity tasks. By creating expert-labeled benchmark data and publicly disclosing evaluation methodologies and AI performance via competitive leaderboards, PRAXIS creates strong incentives for frontier AI labs to advance their models’ verification capabilities – ultimately shifting the balance of cyberwarfare back to defenders.
The initial phase focuses on fully-automated parser retrofitting by testing an AI model's ability to perform two complex tasks: identifying parser functions hidden within a codebase, and extracting formal grammar specifications from those components. Galois engineers are generating manually-annotated ground truth data to validate the models, ultimately creating a rigorous evaluation framework and leaderboard to measure the defensive capabilities of frontier AI models.
We chose to start with parsers for two main reasons: first, parsers are a high-value security target, serving as the first line of defense against malformed or malicious inputs – a challenge DARPA has pursued for years through programs such as HACMS, SafeDocs, and the broader V-SPELLS; second, parsers offer a comparatively tractable starting point because parsing is a well-studied problem and grammars provide a precise, structured representation that makes it easier to test the correctness of lifted specifications.
Value Add
- Leveling the Cyber Playing Field: Enables automated application of formal methods safe parser generation at scale, neutralizing AI-accelerated offensive threats with machine-speed defenses.
- Faster, Cheaper, More Accessible Formal Methods: Automates the most complex, labor-intensive phases of proof engineering – democratizing formal verification so software teams without specialized formal-methods training can secure critical codebases.
- A Path to Trustworthy AI: Establishes mathematical formal verification as an objective ground truth for AI-outputs, guaranteeing software correctness in high-stakes environments.
- Incentivizing Frontier AI Labs: Establishes high-impact, relevant benchmarks and competitive leaderboards that channel the momentum of leading AI labs towards solving critical defensive security challenges.
- Eliminating Critical Vulnerabilities: Lays the groundwork for fully automated parser retrofitting, systematically neutralizing exploit vectors caused by malformed inputs – including remote code execution (RCE), denial of service (DOS), and privilege escalation.
- Extensible Evaluation Ecosystem: Integrates with industry-standard frameworks to deliver a uniform pipeline capable of benchmarking AI across everything from isolated parser identification to end-to-end legacy modernization.
.png)
