John V Siratt

Dr. John V. Siratt is a Research Computer Scientist in the Langley Formal Methods Research Group, part of the Safety-Critical Avionics Systems Branch. He earned his Ph.D. in mathematics from the University of Notre Dame, specializing in mathematical logic under the supervision of Peter Cholak. He also holds an M.S. in applied mathematics.

Dr. Siratt first joined the Formal Methods group as an intern in 2017 and 2018 while completing his master's degree. He returned to NASA through the Pathways Program in 2021, and transitioned to his current role in 2024 following the completion of his doctorate.

His research focuses on formal methods for assurance of complex systems, with a growing emphasis on the verification of machine learning. As part of System-Wide Safety's Technical Challenge 4 (SWS-TC4), he extended theoretical results to characterize the behavior of ReLU-activated classifiers of arbitrary depth, anchoring their expressive power in first-order arithmetic.

Currently, Siratt contributes to Aerial AId, a project under NASA's Convergent Aeronautics Solutions (CAS) initiative that supports drone-based emergency response (Drones as First Responders, or DFR). He leads development of tools for the formal verification of convolutional neural networks (CNNs), including a PVS and Typed Racket based formal model of convolution operations.

He is also the author of the generic matrix and vector formalization in NASA's PVS Library. This supports parametric instantiation of matrix and vector types and dynamic dimensionality, making it well-suited for low-level modeling of neural networks valued in real, fixed point, or floating point, and flexible enough to support non-numeric types like strings. His work bridges rigorous theory and practical tooling, informed by years of experience with logic, formal verification, and aerospace system safety.