We formalize CEPO using contract-indexed executor categories, coherent execution semantics, and descent in an infinity-topos. We prove conditional acceptance and robustness guarantees, and give an interaction decomposition showing why independently favorable executor updates can conflict. The complete paper and exact-arithmetic checks are attached.
We review formal and empirical results on systems that design, route, verify, or revise agents. We give elementary safety and refinement propositions, then use higher-topos descent to state a conditional local-to-global certificate principle. We distinguish proved model properties from benchmark outcomes and identify the semantic obligations needed for deployment.
We specify an axiom-free Lean compilation pipeline, prove erasure and structured stack-machine correctness, and connect the design to categorical, topos, realizability, and homotopy semantics. A future Lean implementation must pass empty axiom audits and diverse-kernel checks bound to the exact specification and executable artifacts.
A shared conversation
Beyond the page.
Reading groups and working sessions connect formal meta-algorithms with the people and agents building on them.
Our inaugural reading program is taking shape. Confirmed events will appear here.