Look-ahead bias—using information from after a decision epoch to make the decision at that epoch—is the dominant way a backtest, a machine-learning evaluation, or a code-change risk metric flatters a system that disappoints in deployment. In quantitative finance it is called look-ahead bias; in machine learning it is one species of data leakage; in software-change prediction the clearest instance is a metric that grades a session's changed files against a snapshot taken before the session ran, so that any file the session created lands automatically in the "surprise" set and corrupts the accuracy figure—the entity was "born inside the measurement window," and no scoring logic can make it a legitimate hit.
Two complementary strands are merged here. The first is a formal account, in which look-ahead-freedom is a formal property in disguise: once an epoch is fixed, the demand that the future not influence the present is temporal non-interference over a time-indexed information lattice. From this identification the authors develop a pipeline calculus that separates a datum's availability (when it can be read) from its reference time (which instant it describes). Look-ahead-freedom is then an instance of non-interference in which the protected "high" partition is the future relative to a decision epoch t, the observable "low" output is the decision at t, and the ordering is temporal availability rather than security clearance. On the full pipeline language U, where availability may be computed from data values, look-ahead-freedom is undecidable—indeed Π⁰₁-complete, with non-look-ahead-freedom recursively enumerable. On the value-independent fragment F, which covers windowing, resampling, joins, point-in-time and vintage reads, and agentic retrieval, the property is soundly and decidably checkable in linear time. Empirical validation on a public clean-room artifact confirms linear scaling, an independent oracle witnesses no leak in any accepted pipeline, and the checker catches all 33 planted adversarial leaks that differential and tiling detectors miss.
The second strand is a Day-206 self-audit of a personal risk-scoring ledger that tested the "born-inside-the-window" artefact thesis by cross-checking a validation ledger against a separate first-seen ledger, together with four published sources on how prediction systems handle newly added files. The audit found the artefact class real in principle—and confirmed in at least one measured case—but on that ledger (≈1 in 55 zero-accuracy rows), and it found its own artefact story unverified where two instruments disagreed about a file's birth date.
rare
Key Points
Every datum carries two independent temporal coordinates: reference time (which instant it describes) and availability (when it becomes knowable). These differ by an ingest lag. A decision at epoch t may legitimately consume a time-indexed value ⟨v, α⟩ only when α ≤ t.
Look-ahead occurs precisely when a datum whose availability follows decision epoch t influences the decision made at t. The general formulation: the decision at time t must not depend on information from t′ > t.
Concrete leakage examples: a normalisation fitted on the whole sample; a feature aligned to the wrong timestamp; a restated fundamental read at its final rather than as-first-reported value; a universe assembled from firms that survived; executing at the signal-generating close versus the next tradable price; forming a universe from future constituents; omitting costs.
The structural artefact in software-change prediction: a grading event compares a session's changed src/ files against a snapshot's top-10 list, scoring each file as a hit or surprise and printing one accuracy_pct. When a file is created by the very session being graded and the snapshot predates the session, that file can never be a hit — it is a spurious surprise and a source of look-ahead bias in the metric.
A "surprise" produced not by a bad prediction but by the structural impossibility of a hit is a spurious surprise. In-window entities (items coming into existence between snapshot and graded event) are the mechanism.
The audit's second instrument (a first-seen ledger) left the artefact story unverified: of 55 zero-accuracy events in the arbiterable window, exactly one had a surprise whose path was first scored after the event. The ledger also placed the disputed file's first-seen date 30 days before the event, contradicting the artefact claim.
Backfilled ledger rows are a survivor/denominator trap: 98 pre-ledger events show the same "first scored later" shape, but every one is an artefact of the ledger's own start date and cannot be read as evidence.
Current practice uses construct-specific recipes—fit transforms on training folds only, lag running statistics, split chronologically, embargo around test windows—and empirical detectors. A recipe is sound only for the specific channel it addresses; a detector reports the leaks it happens to trigger and certifies nothing by its silence.
The paper's formal route: language-based information-flow security supplies non-interference; its timed branch is undecidable for general timed automata but decidable on identified subclasses. Replacing the security lattice with a time-indexed one gives look-ahead-freedom as temporal non-interference.
The language is stratified by whether availability may depend on data values. On U, availability can be value-dependent and look-ahead-freedom is undecidable (Theorem 3, Π⁰₁-hard). On F, availability is value-independent; the property is sound and decidable in linear time (Theorems 1 and 2), and membership in F is itself checkable in linear time.
The type-and-effect system is proved via a two-run logical relation whose crux is re-stamping—the channel by which a future value can be relabelled to an admissible time. Precision is characterised exactly, including opaque-value-operation cases where a sound analysis must conservatively reject a semantically clean pipeline (Proposition 2).
Series operators—windowing, scans, joins, resampling—are hardened. The genuine leakage channel is non-causal resample/join alignment, discharged by an explicit O(1) checker obligation. Base series must be declared availability-monotone; each resample must carry a causal ρ with max ρ←(p) ⪯ ι(p); each join must align sources at a common position.
The contribution is framed as a single conversion: empirical detectors answer "did this pipeline, on the data and epochs I tried, exhibit a leak?", whereas this property answers "can this pipeline, on any data and at any epoch, exhibit a leak?"—soundly, and decidably in linear time on the pipelines practitioners actually write.
Empirical results: linear scaling measured log–log slope 1.023, 95% bootstrap CI [1.021, 1.026], across four orders of magnitude; on five archetypes from proprietary, non-redistributable market data, an independent dynamic oracle witnessed no leak in any accepted pipeline; on an adversarial corpus the checker missed none of 33 planted leaks, while a differential two-run detector missed 18 (54.5%) and a window-tiling detector missed all 33 (100%).
Clean-case false positives: the checker falsely rejected 15 of 20 (75%)—exactly the FP1 and FP2 opaque-value-operation cases—while accepting all five FP2b cases. The two-run and tiling detectors false-positived on none, as expected of tools that only flag observed output changes.
Statistical analysis was pre-registered: cluster bootstrap, cluster-respecting permutation tests, Benjamini–Hochberg correction leaving adjusted q-values at 10⁻⁴, and Wilcoxon signed-rank agreeing at p < 10⁻³. Checker-versus-two-run post-hoc power was 76.7%. Scope caveat: the corpus is adversarial, so results are existence-and-robustness evidence, not estimates of leak frequency in naturally occurring pipelines.
Published predictors differ in treatment of in-window (newly added) files: three of four explicitly exclude or separately rank them (ConEA, the PR risk-review paper, NeuroJIT); the fourth (look-ahead-freedom as temporal non-interference) generalises the whole problem into a formal constraint.
Publication details: Xavier Fonseca, Academy for AI, Games and Media, Breda University of Applied Sciences, The Netherlands; ACM Trans. Softw. Eng. Methodol., Vol. 0, No. 0, Article 0, July 2026, 30 pages; arXiv:2607.04958v1 [cs.CR], 6 Jul 2026.
Concepts
Reference time, availability, and admissibility. Sorts: τ ::= Time | Val | TVal. A time-indexed value is ⟨v, α⟩, where v is an ordinary value and α ∈ Time is its availability stamp. The stamp records when v becomes knowable, not when it is about. A datum ⟨v, α⟩ is admissible at epoch t if α ≤ t.
Availability sublanguage A. Availability terms denote elements of Time and are built only from other availability information, never from values: A ::= t (current decision epoch) | c (constant stamp) | av(x) (availability of a bound time-indexed variable x). The fragment F is the value-independent fragment in which availability cannot depend on data values.
Stratification of the language. On U, the availability argument of a stamping construct may be a pipeline term of sort Time computed from data values—e.g. if val(e) > c then τ₁ else τ₂. On F, availability is confined to A. Lifting the value-independence restriction is shown to be the sole source of undecidability.
Agreement up to t. Two input assignments I and I′ agree up to epoch t, written I ≈_t I′, if they assign identical time-indexed values to every base datum and identical entries to every store entry whose availability is ≤ t. No constraint is placed on data with availability > t. ≈_t is an equivalence relation for each fixed t and is monotone in the epoch: t′ ≤ t and I ≈_t I′ imply I ≈_t′ I′.
Look-ahead-freedom (Definition 8). A pipeline term e is look-ahead-free if for every epoch t, every decide_t subterm with body e′, and every pair of input assignments I ≈_t I′, if I ⊢_t decide_t(e′) ⇓ ⟨v, α⟩ and I′ ⊢_t decide_t(e′) ⇓ ⟨v′, α′⟩, then v = v′. The decision's emitted value is invariant under any perturbation of data whose availability exceeds t. The decision's stamp is t by E-Decide and so agrees across the two runs unconditionally.
Look-ahead bias / temporal non-interference. The decision at time t must not depend on information from t′ > t. This is the applied name for the same failure that the formal account calls temporal non-interference.
In-window entity. An item (e.g. a newly created file) that comes into existence between the snapshot and the graded event. Because it was not available to the predictor, treating it as a miss is a structural artefact rather than a predictive error.
First-seen ledger. An append-only record of every path a scorer has ever observed and when; distinct from the validation ledger that grades events.
Backfill artefact. Rows stamped at the moment a ledger was introduced, whose timestamps reflect the backfill, not real observations.
Survivor/denominator trap. Reasoning from a population whose membership was itself shaped by the measurement boundary—here, pre-ledger events whose apparent "first scored later" shape is an artefact of the ledger's start date.
Spurious surprise. A "surprise" produced not by a bad prediction but by a structural impossibility of a hit.
Operational semantics. Evaluation is a big-step relation I ⊢_t e ⇓ r. Rules include E-Base, E-Val (projection discards the stamp), E-Op (pure operation), E-Stamp (re-stamping replaces the stamp with the denotation of A, leaving the value untouched), E-Asof (point-in-time read returns the applicable store content selected as of the denotation of A, stamped with 〚A〛; retrieve evaluates identically over the agentic context store), E-Decide (decision at epoch t evaluates its body at that same epoch and emits the result), and E-Let.
Monotonicity and causality lemmas. Lemma 5 (monotonicity preservation): if every base series is availability-monotone, then window_k(ē), scan(f, e₀, ē), join(ē₁,…,ēₙ), and resample_ρ(ē) preserve monotonicity under the stated conditions. Lemma 6 (causality): for an F series built from monotone base series by window, scan, join, and causal resample, every position p depends only on base-series elements at positions ⪯* p, and its stamp equals the max availability over those reachable base elements—exactly the effect φ assigned by typing rules T-Window, T-Scan, T-Join, T-Resample.
Undecidability boundary. Theorem 3: look-ahead-freedom is undecidable for terms of U, and the set of look-ahead-free terms is Π⁰₁-complete. Non-look-ahead-freedom is Σ⁰₁: a leak is a finite witness—an epoch t and two assignments I ≈_t I′ differing on a datum of availability > t that yields different decisions at t. The proof reduces the halting problem using three modelling assumptions: M1 value-conditioned availability, M2 configurations as values, and M3 countable position domains.
Details
Applied context and the formal calculus
The applied literature treats look-ahead bias as one of a family of evaluation failures alongside survivorship bias, backtest overfitting, transaction-cost neglect, and regime-shift blindness. LLM migration into trading sharpened it: a taxonomy-oriented evaluation of financial multi-agent systems argues coordination and evaluation protocol, not model scale, drive measured performance, and that claims across systems are hard to compare; an audit-oriented evidence map of LLM trading agents finds acute protocol incomparability, with only a small minority of surveyed empirical studies documenting time-consistent train/test splits, explicit transaction-cost models, or survivorship handling, and none reaching the highest reproducibility tier. Work on execution assumptions makes the mechanism concrete: mundane choices—executing at the signal-generating close versus the next tradable price, forming a universe from future constituents, omitting costs—can move a strategy from apparently profitable to unusable, and retrospective leakage can overturn a strategy's apparent edge. For agentic pipelines the channel is subtler: an agent can leak future information through its pretraining data or retrieval corpus even when its code is fed only contemporaneous inputs—a look-ahead form with no classical analogue that code inspection cannot rule out. Benchmarks quantify performance decay once a model's knowledge window ends, some at claim-level granularity using Shapley attribution to isolate which parts of a rationale draw on post-cutoff information.
The calculus separates availability from reference time at the level of syntax: a datum's value may depend on other data freely, but in the decidable fragment a datum's availability may not depend on any data value. This separation makes availability statically tractable and is justified by how real pipelines are built—availability is exogenous, fixed by the data source (a publication date, a filing date, a bar close), and ingested immediately and unconditionally; a well-formed pipeline never re-times a datum's availability on the basis of another datum's value. The two-level grammar makes this precise, and membership in the decidable fragment is checkable in linear time.
Rendering diagram…
The static discipline is a type-and-effect system: every accepted F-pipeline is free of temporal leakage (Theorem 1), and acceptance is decidable in time linear in pipeline size under bounded availability-term complexity (Theorem 2). The proof uses a two-run logical relation; re-stamping is the crux, because it is the channel by which a future value can be relabelled to an admissible time. Precision is characterised exactly, including opaque-value-operation cases where a sound analysis must conservatively reject a semantically clean pipeline. For series operators, the hardening surfaces two syntactic local obligations: base series must be declared availability-monotone—trusted at ingestion, with incorrect source stamps out of scope—and each resample_ρ must carry a causal ρ, while each join must align sources at a common position rather than across a look-ahead offset. A non-causal alignment is rejected. Both obligations are O(1) per operator, preserving the linear-time bound.
The dynamic meaning is fixed by an epoch-parametrised big-step evaluation, the notion of two inputs agreeing up to an epoch, and look-ahead-freedom as a two-run temporal non-interference property. An input assignment I gives each base datum a time-indexed value I(⟨d, A⟩) = ⟨v, α⟩, where α = 〚A〛. For vintage constructs, I also provides a store: time-indexed entries each carrying availability, over which asof and retrieve read. 〚A〛_{t,I} depends on I only through the stamps of referenced data. A time-indexed value ⟨v, α⟩ is admissible at t if α ≤ t. This semantic content is what the effect discipline approximates statically. The reference-time versus availability distinction is operational: the position of a value in a series and the reference period it is about are recorded in its value/position; availability α records only when it becomes knowable, and it is α—not the reference time—that bounds admissibility.
The undecidability proof is a many-one reduction from the halting problem. For a Turing machine M run on blank input, one constructs a term e_M ∈ U with M halts iff e_M is not look-ahead-free. The position domain is identified with the epoch grid—position p corresponds to epoch p, data at position p has availability p. A causal fold scan(step, cfg₀, ¯ι) computes configuration cfg_p = step^p(cfg₀); by causality, cfg_p is admissible at epoch p. A total pure halting predicate yields h_t = halted(cfg_t), admissible at t and monotone once true. A genuinely future base datum d↑ has natural availability t+1 > t; it is re-stamped with A_t = if h_t then t else t+1, giving d★ = stamp(d↑, A_t), and its value is fed into the decision at t: e_M = decide_t(g(val(d★))), where g is non-constant in its argument. If M halts at step T, then at t = T, h_T = true, A_T = T, d★ becomes admissible and perturbing d↑ changes the emitted value, so e_M is not look-ahead-free. If M never halts, h_t = false for every t, A_t = t+1 > t at every epoch, d★ never influences any decision, and e_M is look-ahead-free. Hence halting reduces to non-look-ahead-freedom. Non-look-ahead-freedom is recursively enumerable and Σ⁰₁-hard; look-ahead-freedom is Π⁰₁-hard and, with the upper bound, Π⁰₁-complete.
The paper situates itself at the intersection of three literatures. Information-flow security, surveyed by Sabelfeld and Myers, supplies non-interference; enforcement mechanisms include information-flow type systems, taint tracking, and gate-level information-flow tracking. Its timed branch has defined notions on timed automata, where timing constraints can turn a secure system insecure and where timed strong non-deterministic non-interference is undecidable in general while cosimulation-, bisimulation-, and state-based variants are decidable. The "undecidable in general, decidable on a subclass" pattern recurs in parametric timed opacity, where general parametric timed automata are undecidable and the L/U-PTA subclass is decidable. This literature supplies a definition schema, enforcement mechanisms, and a known decidability frontier, but has never been applied to look-ahead bias: in prior treatments the "high" partition is a secret protected from an adversary, never data from the future withheld from a decision made in the past.
Provenance and dataflow/stream correctness come closest but do not fill the gap. Scientific-workflow provenance records derivation, distinguishing prospective provenance (workflow specification) from retrospective provenance (executed run), representing causality as a dependency graph; the community standardised these notions in OPM and W3C PROV and separates why- from where-provenance. Provenance records which inputs produced an output but carries no time-indexed admissibility condition: it cannot say an input was drawn from a timestamp later than the output's decision time, and it defines no violation. Even temporal attribution remains descriptive: it reports what did flow, not what may flow across the availability boundary. The dataflow model formalises correct processing of unbounded, out-of-order data using watermarks and timers. The Causify DataFlow framework states the exact hazard—computations at time t may access observations from a later time t′ > t, called future-peeking—and defines causal computation and point-in-time idempotency, proving tilability and tile-correctness results that guarantee batch execution equals streaming execution. But causality itself is detected, not proved: violations are surfaced through testing and replay, validated by tiling tests that partition data in multiple ways, a differential-testing oracle that compares batch against streaming or across tilings. There is no soundness theorem certifying a computation causal. The paper's decisive distinction is what receives a proof: DataFlow proves point-in-time idempotency and tilability by construction but detects causality empirically; this work gives a sound static property whose accepted pipelines are provably look-ahead-free, available only on a decidable fragment—which is, in a precise sense, the best possible because certifying look-ahead-freedom is not recursively enumerable on the full language.
The artifact contains the checker, baseline detectors, the dynamic oracle, the adversarial corpus, and synthetic data on which every qualitative result can be re-run. Headline figures are computed from proprietary market data that cannot be redistributed; the artifact reproduces the method and qualitative claims, not those exact figures. The 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. Table 2 reports detection over the adversarial corpus: false-negative rate over 33 leak cases and false-positive rate over 20 clean cases. The checker's zero-false-negative arm is reported with its rule-of-three upper bound: 0/33, 0.0%, 95% CI [0, 9.1%]. The two-run detector misses 18/33, 54.5%, and the tiling detector misses 33/33, 100.0%, CI [100, 100]%. On clean cases the checker false-positives on 15/20, 75.0%—FP1 and FP2 only, with FP2b accepted—while the two-run and tiling detectors false-positive on 0/20, 0.0%. An alignment anchor exhibits the same detector-miss phenomenon on real market data; in the released artifact this anchor is replaced by a synthetic term with the same alignment structure.
Inference follows a pre-registered plan. Primary endpoints are pairwise false-negative differences between each detector and the checker; secondary endpoints are the false-positive comparison and non-parametric robustness. Because the corpus is clustered by mechanism, inference uses a cluster bootstrap and a cluster-respecting permutation test rather than treating cases as independent. For the two dominance comparisons, the checker misses strictly fewer leaks than the two-run detector (difference 54.5 percentage points) and than the tiling detector (100 points); a 10,000-draw permutation test rejects equality in both cases, and because the checker arm is perfect the permutation statistic sits at its resolution floor, so the paper reports p < 10⁻⁴ (permutation-limited) with the number of discordant pairs (18 and 33 respectively). A Benjamini–Hochberg correction over the family leaves all adjusted q-values at 10⁻⁴. A Wilcoxon signed-rank test on paired per-case correctness agrees (p < 10⁻³ for each comparison). Post-hoc power for checker-versus-two-run is 76.7% at the observed effect, below the conventional 80% and reported as such; the small corpus limits power while the permutation and Wilcoxon tests independently corroborate the effect, and checker-versus-tiling is at maximal effect. Scope caveat: the corpus is adversarial, so these rates are existence-and-robustness evidence—leaks of these kinds exist that defeat the detectors and are caught by the checker—not estimates of leak frequency in naturally occurring pipelines. Two pre-registered deviations are recorded: subgroup bootstraps resample within the leaking or clean mechanisms respectively.
The grading mechanism under audit
A risk ledger (.yoyo/risk_validations.jsonl) had graded 267 events, scoring each session's changed src/ files as hits (present in the snapshot's top-10) or surprises (everything else), and printing a single accuracy_pct. It is written by auto_validate_after_failure_to / record_green_validation_to in src/commands_risk_snapshots.rs. The audit read this claim against a second, previously unused instrument: .yoyo/risk_first_scored.jsonl, an append-only ledger of every path the scorer has ever seen and when (writer append_first_scored_to, via write_risk_snapshot_to).
The artefact mechanism
The core structural fact is temporal: if the snapshot was taken earlier than the graded session, a file created by that session was never available to the predictor, so calling it a surprise penalises the predictor for something it could not have seen.
Rendering diagram…
What the second instrument showed
The first-seen ledger begins 2026-08-22T16:35:02Z with 97 paths backfilled at one timestamp with one git hash — the ledger's own introduction, so those timestamps are the backfill moment, not observations.
Restricted to grading events at/after that start (the only population the ledger can arbitrate): 115 events, 55 with accuracy_pct 0.0. Of those 55, exactly one contained a surprise whose path was first scored after the event — day 203, 2026-09-20T09:46:24Z, src/format/highlight/highlight_tests.rs, first scored at 10:26:23Z (40 minutes later, a real observation with no backfill row).
The row the prior journal actually attached the artefact story to (day 204, src/commands_risk_epistemic_tests.rs) has a first-scored record dated day 175 — 30 days earlier. On the path dimension the artefact story is unverified at best, and two instruments disagree about that file's birth.
98 pre-ledger events show the same "first scored later" shape, but each is a backfill artefact of the ledger's start date and cannot count as evidence — the survivor/denominator trap.
The unresolvable population: 20 surprise entries across the 128 zero rows have no first-scored record at all; 7 zero rows are entirely unrecorded.
Net: the artefact class is real in principle and confirmed in at least one measured case, but on this ledger it is rare (≈1 in 55 zero rows), not the dominant explanation.
How published predictors handle in-window members
Four ingested sources, three of which act explicitly:
Continuous Software Bug Prediction (ConBuild/ConUpdate/ConEA, ESEM'21) — new files in version vn are not present in vn-1 and are handled explicitly rather than silently counted as ordinary rows. Also documents that version-selection randomness alone moves AUC by up to 0.359 on one project.
Look-Ahead-Freedom as Temporal Non-Interference (arXiv 2607.04958) — formalises the constraint that the decision at time t must not depend on information from t′ > t, and observes that detectors report only the leaks they happen to trigger and certify nothing by their silence.
NeuroJIT (DOI 10.1145/3691620.3695056) — dataset cleaning drops commits that add multiple new files, on the stated ground that developers do not engage with those the same way.
Enhanced code reviews using PR-based change impact analysis (EMSE 2024) — states outright: "our analysis does not include newly created files, focusing only on modified or existing ones" — a system that names its exclusion instead of letting a zero absorb it.
Open questions
Does adding a "files absent at the snapshot git hash" field to the validation event make the accuracy number honest, or merely relocate the judgement call?
How should a predictor handle members born inside the measurement window — exclude, separately rank, or clean out entirely?