NeuroTrace: Spec-Aware Neural Network Runtime
Robert Joseph George · Team Safeboy
Submitted to The Secure Program Synthesis Hackathon. Sprint projects are early-stage work by participants, not Apart Research publications.
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.

Reviews
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 project
@misc{george2026neurotrace,
title = {{NeuroTrace: Spec-Aware Neural Network Runtime}},
author = {Robert Joseph George},
year = {2026},
month = may,
note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
howpublished = {\url{https://apartresearch.com/sprints/projects/neurotrace-specaware-neural-network-runtime-mipv}},
url = {https://apartresearch.com/sprints/projects/neurotrace-specaware-neural-network-runtime-mipv}
}More from The Secure Program Synthesis Hackathon
- View project: Vibe-Coding Specs: Eliciting, Editing, and Verifying Specifications for AI Coding Agents
Vibe-Coding Specs: Eliciting, Editing, and Verifying Specifications for AI Coding Agents
Lida Safety
Specifications for real systems do not exist as one-shot artifacts: the user's intent emerges as they discover edge cases, rewrite drafts, and react to failing tests. We present an iterative pipeline that takes this …
- View project: AgentSpecGap
AgentSpecGap
solo-team
This prototype extracts rules from system prompts, tool descriptions, and runtime config. Rules are classified into one of interface validation, authorization check, workflow ordering validation, runtime validation, …
- View project: SpecGap Arena
SpecGap Arena
Obligation Cartographers
SpecGap Arena is a benchmark and framework that exposes how incomplete specifications let plausible but incorrect code pass public tests. It synthesizes missing semantic obligations (security boundaries, invariants, …