NEURA: An agentic system for autonomous neuroimaging workflows

Abstract Neuroimaging research depends on heterogeneous software, multimodal data and multistage statistical workflows. Large language model (LLM)-based agents offer a route to automate these workflows, but their susceptibility to hallucination limits their credibility in scientific use. Here we introduce NEURA, a proof-carrying framework for hallucination-resistant neuroimaging automation. NEURA converts free-text research questions and neuroimaging datasets into executable analysis plans, validated outputs and structured reports. The system combines disease- and tool-aware planning with a deterministic verification layer inspired by formal proof: before any claim is retained for reporting, it must be checked against tool-derived evidence and domain axioms. On NeuroEval, an expert-curated benchmark of 110 neuroimaging tasks, NEURA achieved 89.5% planning accuracy, a 30.5% improvement over direct LLM queries. In a controlled hallucination-injection experiment, the verification layer detected all the injected error classes under the specified axiom bank and trust assumptions, with no false positives. In case studies of spinocerebellar ataxia type 3, NEURA reproduced cerebellar atrophy and abnormal diffusion patterns consistent with established pathology and independent expert analyses. Together, these findings show that coupling domain-grounded agency with proof-carrying verification can turn LLM-driven workflow automation from probabilistic self-checking into auditable scientific computation. Competing Interest Statement The authors have declared no competing interest. Footnotes Major revisions include a new title; a rewritten abstract; expanded Introduction sections on LLM hallucination, LLM-as-judge limitations and formal verification; a new Results section on controlled hallucination injection; revised Overview text clarifying the roles of MoER and the proof kernel; new Methods sections describing the proof kernel, domain axioms, proof construction and hallucination-injection protocol; and a revised Discussion comparing NEURA with workflow engines and scientific agents. The Limitations and Data/Code Availability sections were also updated to address axiom-bank coverage, tool trust boundaries, external validation, and release of the axiom bank, proof kernel and verification resources.