2607.02845 Verifying Sutra as an Execution Environment on a Probabilistic Substrate: Per-Contract Convergence and Closed-Form Obligations for a Compiled Functional Language
We verify **Sutra** — a typed, purely functional language — as a fixed **execution environment**: an instruction-set architecture whose *non-learned* trusted base (kernel roles and named critical programs, behaviour fixed at compile time) runs on a substrate that is, on its second compile target, genuinely **probabilistic** — a sampler that *settles into* the answer rather than computing it deterministically. The claim is narrow and per-contract; we do not claim to verify a learned component or a whole running system.