AI research tools can quietly manufacture results — and a new architecture is designed to make that structurally impossible.
A team of researchers has published a functional architecture that enforces statistical discipline on AI-driven discovery systems at two levels. First, a Haskell embedded domain-specific language called the Research monad makes it impossible to test a hypothesis without debiting an error budget — the accounting is baked into the type system, not left to convention. Second, a declarative scaffold backed by an OS-level sandbox physically removes validation data from the environment where LLM-generated code runs, so a model cannot cheat even if it tries. The statistical backbone is LORD++, an online false-discovery-rate control procedure formalized in Lean 4 — a machine-checked proof that derives the error budget and verifies both marginal and full FDR control. The authors then close the gap to the actual running code by verifying the budget's wealth invariant over IEEE 754 floating-point arithmetic in SPARK/Ada, which they claim is the first verified chain from theorem to floating-point implementation for any online FDR procedure.
The practical gap the paper is filling is real. In simulation, the architecture holds the false discovery rate near 1% against a 5% target; a naive approach hit 41%. That 40-point swing is the kind of error that, in a production AI-scientist pipeline, produces published-looking results that don't replicate. Most current guardrails for AI research tools rely on prompting or post-hoc filtering — neither of which is enforceable at the type or OS level.
The work sits at an unusual intersection: formal verification applied not to safety-critical embedded systems (SPARK/Ada's usual home) but to the statistical contracts inside an AI research loop. Whether the research community adopts a Haskell DSL for this purpose is a separate question from whether the underlying idea is sound — and on the second point, the proof record is hard to argue with.