NeuroTrace: Spec-Aware Neural Network Runtime
Robert Joseph George
NeuroTrace is a spec-driven observability framework for neural network models. The core idea is that a neural specification should not stay as a static file: it should become a live contract that the runtime, training loop, optimized implementation, export artifacts, and verifier outputs must continue to satisfy. NeuroTrace triangulates across TorchLean-style specs, PyTorch hooks, torch.fx, ONNX/VNN-LIB, Marabou, SpecTrace training logs, Fast Path checks, and SpecFuzz mutations to detect when the artifact chain drifts from the intended model. My long-term goal for it is to become a practical “spec observability” layer for ML systems, especially as AI agents generate code and frontier-style systems replace readable models with faster optimized runtimes.
This approach shows promise and is I believe a novel combination and application of these methods. I am excited to see if this scales to real-world bugs and implementation. I also liked the variety of objects covered in the demonstration here and was impressed by the hackathon velocity.
I'd have liked to see more justification or exploration that the autoformalization into the contract is reasonable, since the correctness of this is fairly load bearing for the usefulness of this technique. Additionally, the write-up was a little hard to follow and some key claims or ideas were buried in the stream-of-consciousness format.
Constant surveillance as opposed to a single check seems very promising. But, the human prompt to contract writing using an AI in itself is not a very robust methodology.
Cite this work
@misc {
title={
(HckPrj) NeuroTrace: Spec-Aware Neural Network Runtime
},
author={
Robert Joseph George
},
date={
},
organization={Apart Research},
note={Research submission to the research sprint hosted by Apart.},
howpublished={https://apartresearch.com}
}


