Look-Ahead-Freedom as Temporal Non-Interference: A Verifiable Correctness Property for Backtesting and Agentic Trading Pipelines

Jul 16, 2026

Upload by Noah

Look-ahead bias in backtesting and data leakage in machine-learning evaluations undermine real-world reliability by allowing future information to influence decisions. The work formalizes look-ahead-freedom as temporal non-interference on a time-indexed information lattice, separating datum availability from its reference time. For value-dependent availability, the property is undecidable (Π01-hard), while for value-independent pipelines a type-and-effect system yields sound, decidable checking in linear time. A verified artifact confirms full detection of planted leaks in accepted pipelines.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages30

Reading Time1 h 16 min

Introduction

Reproducibility

arXiv :2607 .04958v 1 [ cs .CR] 6 Jul 2026 Look-Ahead-Freedom as Temporal Non-Interference: A Verifiable Correctness Property for Backtesting and Agentic Trading Pipelines XAVIER FONSECA, Academy for AI, Games and Media, Breda University of Applied Sciences, The Netherlands Look-ahead bias—using information from after a decision epoch to make the decision at that epoch—is the dominant way a backtest or a machine-learning evaluation flatters a system that will disappoint in deployment. The field manages it with construct-specific recipes and empirical detectors, which are sound only channel by channel and certify nothing by their silence. We show that look-ahead-freedom is a formal property in disguise: fixing an epoch, the demand that the future not influence the present is temporal non-interference over a time-indexed information lattice. From this identification we develop a pipeline calculus separating a datum’s availability from its reference time, and settle the problem’s boundary. Where availability may depend on data values, look-ahead-freedom is undecidable (Π01-hard): leakage is recursively enumerable but freedom is not. On the value-independent fragment—covering windowing, resampling, joins, point-in-time and vintage reads, and agentic retrieval—we give a type-and-effect system that is sound and decidable in linear time. An artifact confirms the theory: the check scales linearly, an independent oracle witnesses no leak in any accepted pipeline, and the checker catches every planted leak that differential and tiling detectors miss.1 CCS Concepts: • Software and its engineering → Software verification and validation; • Theory of computation → Type structures; Program semantics; • Security and privacy → Information flow control. Additional Key Words and Phrases: look-ahead bias, data leakage, non-interference, type-and-effect systems, decidability, backtesting, agentic systems, point-in-time correctness ACM Reference Format: Xavier Fonseca. 2026. Look-Ahead-Freedom as Temporal Non-Interference: A Verifiable Correctness Property for Backtesting and Agentic Trading Pipelines. ACM Trans. Softw. Eng. Methodol. 0, 0, Article 0 (July 2026), 30 pages. [https://doi.org/10.1145/nnnnnnn.nnnnnnn](https://doi.org/10.1145/nnnnnnn.nnnnnnn) 1 Introduction A backtest is a claim about a decision that was never made: it reports what a strategy would have decided at each past instant, had it been running then. The claim is only meaningful if each simulated decision used exactly the information available at its own instant and nothing from later. When this fails—when a computation performed for time 􀁃 consumes a datum that only became known after 􀁃—the backtest measures foresight the live system could never have had. In quantitative finance this failure is called look-ahead bias; in machine learning it is one species of data leakage. Under either name it is the dominant way an evaluation flatters a system that will disappoint in deployment, and it is notoriously easy to introduce and hard to see: a normalisation fitted on the whole sample, a feature aligned to the wrong timestamp, a restated fundamental read at its final rather than its as-first-reported value, a universe assembled from the firms that survived. 1Reproducibility. A public artifact accompanies this paper, containing the checker, the baseline detectors, the dynamic oracle, the adversarial corpus, and synthetic data on which every qualitative result can be re-run. The headline figures reported here are computed from proprietary market data that we are not permitted to redistribute; the artifact reproduces the method and the qualitative claims, not those exact figures. See the Data and Code Availability statement (before the references) . Author’s Contact Information: Xavier Fonseca, Academy for AI, Games and Media, Breda University of Applied Sciences, Breda, The Netherlands, [xavier.fonseca.phd@gmail.com](xavier.fonseca.phd@gmail.com). 2026. ACM 1557-7

FAQs

What problem does look-ahead freedom address in backtesting and agentic trading pipelines?

It addresses look-ahead bias and data leakage where future information improperly influences decisions at earlier time epochs, making evaluations unreliable in deployment.

How is look-ahead-freedom formalized in the paper?

By identifying it as temporal non-interference over a time-indexed information lattice, requiring that the future not influence the present.

Is look-ahead-freedom always decidable for any pipeline?

No. When datum availability depends on data values, the property becomes undecidable (Π01-hard). For the value-independent fragment, the paper provides a type-and-effect system that is sound and decidable in linear time.

Jul 16, 2026

Upload by Noah