Advancing Cryptographic Verification with AI: Reflections on my Hiring our Heroes Fellowship at Galois

This summer, I had the opportunity to join Galois as a Research Engineer through the Hiring our Heroes Fellowship Program. Hiring our Heroes is part of the Department of War SkillBridge program that allows active-duty service members to work in industry during their last 180 days in the military. The service member can see what work-life is like outside of the military, while using their military experience and operational knowledge to bring a fresh perspective that is sometimes hard for companies to otherwise find.

I was first introduced to Galois a few years ago while working on several projects modernizing cryptographic systems. Bridging this experience to become the first Hiring our Heroes Fellow hosted by Galois has been an amazing opportunity and a great capstone to my 20-year military career. What I didn’t expect was how naturally two decades of military problem-solving would translate into cutting-edge Artificial Intelligence (AI) research.

Training LLMs to Write Better Cryptol

During my fellowship, I worked on an internal research project called enhanced Formal Methods with Reinforcement Learning (eFMRL). The eFMRL project explored the possibilities around fine-tuning medium language models to improve their performance writing code in domain-specific languages with Cryptol as the first target.

Cryptol is a domain-specific language developed and maintained by Galois. It is primarily used to apply formal methods to analyze and assess cryptographic algorithms. In conjunction with Galois’s SAW suite, Cryptol enables the process of proving functional equivalence between a Cryptol specification and a particular implementation in another language like Rust or C. This type of formal verification is important because a proved equivalence is a mathematical guarantee that the implementation is correct. This is far stronger evidence for correctness than simply passing functional tests that could fail on edge cases.

Large Language Models (LLMs) have trouble writing syntactically-correct Cryptol specifications because the publicly available training data does not contain much Cryptol code. This scarcity exists because Cryptol is primarily used in high-security research and defense contexts, where code is often proprietary or classified and never makes it into the public repositories that LLMs train on. This is a critical challenge because cryptographic code is uniquely unforgiving. Improper cryptographic implementation can expose sensitive data or communications without any obvious indication that something is wrong.

As the pace of development increases with the use of AI, the ability of human software engineers to review code for correctness is also a significant bottleneck. Enabling AI to also write valid specifications in a domain-specific language like Cryptol is an important step toward automating our ability to prove the correctness of AI-generated code. This automation will alleviate the bottleneck with tooling that can not only generate code, but prove its correctness and produce human-readable artifacts that make it far easier for developers to audit and trust the results. Doing this with a medium language model means that the tooling is small enough to be deployed into resource-constrained environments like air-gapped development enclaves where access to frontier models is costly or infeasible.

As the developers of Cryptol, Galois is uniquely positioned to solve this problem. Using the limited publicly available Cryptol examples and Galois’s internal repositories, we built a dataset to challenge the models in both writing Cryptol from scratch and fixing broken Cryptol specifications. For the latter, I used Python to write a permuter that takes valid Cryptol specifications and breaks them by changing syntax and removing essential elements of the code.

Building a Training Pipeline

Once the dataset was built, we needed a target model to train. We started looking at the publicly available open-weight models, and settled on OpenAI’s GPT-OSS 20b and Google’s Gemma 4 26B-A4B-it. These models are large enough to perform well on programming tasks, but small enough to host locally. This is important because we targeted deployment scenarios that may not include the robust hardware necessary to host a frontier model. We also used the Gemma 4 E2B-it model in development because it is significantly smaller and faster than the other two models. This enabled us to move faster as we were testing and debugging the training pipeline.

Fine-tuning a language model is not a straightforward task as there are many different technology options and the “best” option frequently depends on the specific use case. The project’s 128 GB DGX Spark could not support the memory demands of traditional reinforcement learning pipelines with a 60 GB model, so we looked specifically at ways to reduce the training time and resource requirements. Three technologies stood out: Reinforcement Learning with Verified Rewards, Group Relative Policy Optimization, and Low-Rank Adaptation. I was tasked with integrating them to form a coherent training pipeline.

The primary training method deployed in eFMRL is Reinforcement Learning with Verified Rewards (RLVR). Reinforcement learning (RL) is a technique where the model is rewarded for good performance and, in some cases, penalized for bad performance. This requires a reward function that determines what reward or punishment the model should receive. It is challenging to use vanilla RL on programming tasks because it is not always clear whether or not the model performed the task correctly. By leveraging the Cryptol compiler as a source of truth, the reward function has a clear signal as to whether or not the code the model produced is valid Cryptol. One downside to RL training is that it can be very time consuming as the model tries different things to learn what we want it to do. Our first optimization tackles this challenge directly.

The first optimization technique we layered onto the RLVR pipeline was Group Relative Policy Optimization (GRPO). Training with GRPO requires the model to generate multiple outputs for each prompt, and each output is scored individually. Once scored, the results are combined with a normalization function before backpropagation. By granting the model multiple attempts at each prompt, it does not need as many training cycles to converge and show real training improvements. We trained the models with the temperature (or randomness) turned up to 0.8, but evaluated them with it turned down to 0.2.

Next, we needed to reduce the amount of memory the training pipeline required. Traditional RL techniques load multiple copies of the model into memory which would require significantly more memory than we had available. Low-Rank Adaptation (LoRA) is a technique that creates a small adapter that connects to the model. This LoRA adapter contains weights that are combined with the base model to produce results. The only weights that are trained are the LoRA weights, which can be merged back into the base model once training is complete. Rather than loading multiple copies of the 60 GB model into memory, we only need to load the model and LoRA adapter once. This means we can train the model using approximately 70 GB of memory.

In addition to fine-tuning, we also injected knowledge into the model using a system prompt. There are advantages and disadvantages to both techniques and we wanted to understand the tradeoffs. As such, I developed two different system prompts to help the model get a head start with Cryptol syntax. The first was approximately 300 tokens and the second was approximately 1000 tokens. We trained the base model with each prompt to measure differences in performance.

Outcomes, Impact, and a New Career Chapter 

In training, we discovered that the Gemma model trained much faster than the GPT-OSS model. Given the limited time during my fellowship, we decided to focus our efforts on the Gemma model. All of the evaluations used the same splits of training and evaluation data.

The base Gemma 4 26B-A4B-it model’s ability to successfully write valid Cryptol with no system prompt was an abysmal 44% overall. Adding either the 300 or 1000 token system prompt improved this performance to 65-66%. This is a significant improvement, but still not reliable enough to be very useful in practice.

Training the base model over 600 steps (approximately 50 hours) with the 300-token system prompt improved the success rate to 78%, and the 1000-token system prompt achieved an 86% success rate. The improvement was even more pronounced on the broken-code task, where the 1000-token trained model achieved a 97% success rate compared to the untrained model’s 71%.

A 97% success rate fixing broken Cryptol means the model is approaching a useful threshold where it has the potential to meaningfully accelerate developer workflows. Cryptographic product vendors could benefit directly from this research by deploying the model into their development environments and the model’s small size makes it easier to deploy into more isolated enclaves. This model can lower the barrier to proving cryptographic correctness with Cryptol by enabling developers to create Cryptol specifications more rapidly. Our next steps for the project will include testing the model’s ability to fix its own broken code, and how our pipeline generalizes to other domain-specific languages like DaeDaLus, Lean, PVS, and Verilog. We are also exploring ways to integrate this model into other Galois tools.

This research was a natural fit for the type of experience the Hiring our Heroes fellowship is intended to produce. Twenty years of operating under constraints and delivering results when the path forward isn’t clearly defined turned out to be useful preparation for building novel AI tooling on a tight timeline. The fellowship has been an ideal way to close out my Army career while opening a new one, and I am proud to have been Galois’s first Hiring our Heroes Fellow. I look forward to continuing this research as a full-time Galwegian, building tools that reduce the cognitive burden on developers and strengthen security across the cryptographic ecosystem.