Ariel Kellison
Code Metal Inc.
ak2485@cornell.edu
Bio
Ariel Kellison is a Senior Research Engineer at Code Metal, where she applies her expertise at the intersection of programming languages, formal verification, and numerical analysis to the development of LLM-based transpilers. She received her Ph.D. in computer science from Cornell University in 2024 and subsequently held a postdoctoral appointment at Sandia National Laboratories. From 2020 to 2024, Ariel was a Department of Energy Computational Science Graduate Fellow, and in 2025 she was named a Frederick A. Howes Scholar in Computational Science, one of the DOE’s highest honors for emerging leaders in the field. She holds a Bachelor of Science with honors in astrophysics from the University of California, Santa Cruz.
Areas of Research
- Programming Languages
Formal Methods for the Age of Approximation
Software systems increasingly operate under approximation: they rely on inexact arithmetic, noisy inputs, and, more recently, code produced by large language models (LLMs). In some sense, all ages are ages of approximation, since scientific and engineering practice has always depended on models that simplify reality. What makes the present moment distinctive is today’s reliance on low precision floating-point computation, noisy data, and generative AI, which makes correctness under approximation more urgent than ever. These systems are entrusted with high-stakes tasks such as steering vehicles, guiding public policy, and shaping scientific discovery. Traditional formal methods often falter at this intersection of scale and approximation, either failing to capture the effects of inexactness or collapsing under the size and complexity of real programs. My research develops principled methods for ensuring correctness in these settings by drawing on programming language design, formal verification, and numerical analysis to build tools that provide guarantees for software ranging from scientific simulations to industrial LLM-based transpilers. Grounded in formal methods but shaped by collaborations in scientific computing and AI, my work bridges theory and practice. My vision is to advance scalable techniques for reasoning about program behavior under approximation and to embed correctness into scientific and engineering workflows where reliability is crucial but often overlooked.