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. 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 a