A New Software Paradigm: Trained Systems, Large Language Models, Agents, Verification Harnesses, and Proof-Carrying Software

Abstract

Software is no longer only written; increasingly it is trained. The artifact this produces is not syntax given meaning by an operational semantics but a probability law coupled to an environment---and none of the classical guarantees survive the change unmodified. This paper supplies the mathematics of the new object. Five postulates define the trained-software paradigm: the artifact is a trajectory law, not a weight vector; identity is functional and deployment-relative; every property claim arrives through an evidence channel with bias and variance; release is a decision with an abstention option; and composition is contract-guarded coupling of laws. Classical software is recovered as the deterministic, oracle-observed boundary case. The postulates are load-bearing: they yield three theorems the model-only view cannot state.There is no such thing as a model's benchmark score---attribution to weights alone is ill-posed until scaffold, decoder, context, and budget are fixed. Memory is a budget---a $B$-bit compressed state cannot separate more than $2^B$ task hypotheses, and the value lost admits a Fano lower bound. And search is never free---under an exponential verifier tail, breadth $K$ pays averification tax of order $\log K$ per candidate, so controlled search satisfies $K\log K\asymp cC$ and verifier quality $c$ multiplies effective compute. Around this core the paper builds a unified analytic treatment: one controlled stochastic recursion specializes to pre-training, post-training, and agent learning, and supports exact results on variance-optimal sampling, compute-optimal allocation, Gibbs post-training, adaptive testing, distributed drift, and numerical perturbation, each with visible hypotheses. Executionfeedback is treated as statistical evidence, not a semantic oracle: search reduces random error while amplifying systematic verifier bias. Release becomes a derivable judgment in a five-rule deployment calculus with a proved soundness theorem, serialized as certificates and enforced by a harness with a formal transition semantics; a Lean~4 companion machine-checks the algebraic and inductive proof kernels. A repository-agent case study connects the abstractions to practice. The result is a design calculus for training and accepting learned software under finite data, compute, and verification budgets.