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

Battle Count: 50

Directly addresses the dominant failure mode in quantitative trading evaluation: look-ahead bias in backtesting. Provides the first formal, verifiable correctness property certifying that a trading pipeline (including agentic LLM-based systems) does not use future information at decision time. Covers all major leak channels: windowing, resampling, joins, point-in-time/vintage reads, survivorship, and agentic retrieval. The linear-time checker is practically deployable. The undecidability boundary precisely characterises what can and cannot be certified. Highly relevant to backtest validation, feature engineering, and LLM-based trading agent evaluation.

Requires understanding of type-and-effect systems, information-flow security theory, and formal semantics. The checker itself is linear-time and syntactic (single bottom-up pass), making runtime implementation tractable. However, expressing real pipelines in the calculus requires modelling availability stamps, causal alignment, and monotonicity invariants. The two-level grammar and effect normalisation add conceptual complexity. Integration with existing backtesting frameworks (not yet available) would require significant engineering. The theoretical results (soundness proof via two-run logical relation, undecidability via halting reduction) are mathematically sophisticated.

A public clean-room artifact accompanies the paper containing the checker, baseline detectors, dynamic oracle, adversarial corpus, and synthetic data. All qualitative results can be re-run end-to-end. However, headline figures are computed from proprietary market data not redistributable under license. The artifact ships synthetic stand-ins reproducing the same leak mechanisms. Pre-registered analysis plan committed before statistical code was written. All seeds fixed. Committed at revision fcc6a41. One methodological deviation (quadratic-to-linear normalisation fold) documented transparently.