Correct-by-Construction Factor Computation: A Verifiably Point-in-Time Engine for Tradeable Signals

PITROVE is a factor-computation engine built on a single principle: point-in-time (PIT) correctness is a verifiable construction invariant, not a claim. The engine couples a declarative, self-describing predictor specification with a non-bypassable validation gate that admits a signal to the feature store only if it satisfies five invariants: temporal causality, finiteness, key-uniqueness, non-degeneracy, and freshness. Most accounting signals are attached by an announcement-date backward join, which closes availability-timing leakage; same-period cross-sectional signals instead use a stronger statutory-deadline release rule that blocks both restatement leakage and the incomplete-cross-section leakage that naive as-of joins miss, demonstrated on the abnormal-accruals construction.Using the Open Asset Pricing catalogue as a standardized, reproducible workload — the role TPC benchmarks play for database systems — we instantiate 150 of its 212 predictors as 160 daily signals over 2,222 Taiwan-listed securities and roughly 8.0 million firm-day observations each. Every one of the 160 series records zero look-ahead violations, zero non-finite values, and zero duplicate keys, and the engine rebuilds the entire library (~1.3 billion signal values) from raw data in approximately sixteen minutes on a commodity workstation. A leakage-injection positive control establishes that the gate has discriminating power.We are explicit that this certifies integrity rather than profitability. A controlled experiment shows the statutory-deadline rule removes a systematic cross-sectional bias left in place by a naive announcement-date join. A real-Taiwan ablation on two cross-sectional signals finds the leakage-specific component is not detectable above finite-sample noise, indicating that this channel adds estimation noise rather than spuriously inflating performance. As an end-to-end demonstration that one codebase serves both research and production, a net-of-fee momentum signal generated by the engine compounds at 26.3% annually (Sharpe 1.24) against 12.0% for the market over twenty-one years. Beyond finance, the five invariants and the statutory-deadline release rule constitute a general assurance technique for any pipeline that derivestime-stamped features from staggered, revisable, cross-sectional inputs, including the construction of training and evaluation data for machine-learning systems, where temporal leakage is a well-documented failure mode (Kaufman et al., 2012). The non-bypassable build gate and the leakage-injection positive control are, in this sense, data-processing and assurance techniques; the equity-factor catalogue is the workload on which they are demonstrated. The contribution is the verifiable, portable, production-scale engine; the anomalies are merely its workload.JEL classification: C55, C58, C88, G11, G17.