The Open Planner: Certified Analytical Plans from Untrusted Searchers — A Research Program Note

We propose an architecture in which the query planner of an analytical system is split into an untrusted searcher — probabilistic, external, possibly adversarial — and a small deterministic kernel that certifies every candidate plan before execution. The kernel discharges two independent obligations: lawfulness (the plan violates no law of the declared, data-adjudicated semantic model) and faithfulness (the plan implements the ask's denotation — plan ⊨ ask). We state a planning-sufficiency theorem: everything required to construct a certifiable plan is contained in the model's public logical projection, so planners are public buildable software and the projection boundary is simultaneously the security boundary. We report an eight-node plan IR extracted from a shipped system (Columna, Apache-2.0); the discovery that the shipped system already contains an uncertified dual-derivation seam the architecture would close; and an executed attack demonstrating a lawful-per-node plan that diverges from the faithful answer by 13–17% monthly (1.21× overall) on public demonstration data. A verified prior-art sweep bounds four regions where no published work was found: a metadata-sufficiency theorem for planning; LCF/PCC-descended kernels over data-adjudicated semantic models; dual lawfulness-plus-faithfulness certificates; certified plan-equivalence as a kernel duty. The governing doctrine: probability is admitted to search, never to adjudication. Version 1.0 stakes the program's claims and evidence as of 2026-07-27; items marked provisional await engine-path reproduction in v1.1.