emberian/svenvs

svenvs is an experimental research project that builds a safety envelope for an AI agent, letting it act and even improve itself while a mathematically checked proof guarantees it cannot break a defined set of safety rules. The idea is to give an AI system a sandboxed place to operate in where every action, including changes the AI makes to its own code, has to pass through a gate that is formally verified: a proof assistant checks the logic step by step before anything is allowed to run. The system is organized into three tiers that build on each other. Tier 1 works with just HOL4, a proof assistant, and includes a working example agent, a cart and pole simulation and a jailbroken language model, contained inside the verified rules. Tier 2 adds a built chain from CakeML's Candle prover, which lets the system prove and recheck its own upgrades. Tier 3 goes further: the core safety proofs are recertified live, while the system is actually running, by the Candle prover itself rather than just checked once ahead of time. The project is unusually direct about what it does not claim. A file called CLAIMS.md lists exactly which theorems are fully proved without assumptions, and which rely on three named assumptions that are spelled out rather than hidden. One of those three assumptions has already been proven true for a specific finite test case, turning it from an assumption into a proved result. Automated checks confirm there are no shortcut proof steps, meaning nothing is marked verified without actually being checked. svenvs is written in Standard ML and depends on the HOL4 and CakeML proof tools. It comes with a two minute demo script that builds the core system, runs the checks, and shows the results directly, along with detailed install and reproduction instructions for anyone who wants to verify the claims themselves rather than take them on faith.