# Compiling Lean specifications into OxCaml enforcement automata *2026-08-01 — idea* [Bastion](https://anil.recoil.org/papers/2024-hope-bastion) is an OS architecture for safeguarded AI where _what_ an agent may do is expressed as a "capability signature". This is an [Dijkstra monad](https://doi.org/10.1145/3341708) whose commands are the only effects the agent can reach, with the indexed monad providing the modular reasoning principles required. This system requires a robust _policy enforcer_ in the runtime system that sits inside the real application and dynamically prevents commands from running that the policy doesn't permit. A long, long time ago I built something just like this in the [Statecall Policy Language](https://anil.recoil.org/papers/2009-icfem-spl) to let a programmer write a protocol automaton (e.g. for SSH or DNS) once and compile it to both Promela (so that SPIN could model-check safety properties expressed in LTL), and to OCaml as a safety monitor linked into the running application that raised an exception the moment the program deviates from its model. The idea here is that a single spec that can be checked is used both for reasoning and also to embed in the real application code, so that the model and the code don't drift apart. The cost of carrying a monitor back then in an [SSH server](https://anil.recoil.org/papers/anil-phd-thesis) was a tiny ~2 of throughput, and it could be made negligible these days. This project aims to apply that idea to modern day proof-oriented programming. We'll do the static reasoning in Leana 4 rather than Promela, and gthe a Dijkstra monad rather than LTL formulae. For the applications, we'll use [OxCaml](https://anil.recoil.org/projects/oxcaml) running inside [Eio](https://anil.recoil.org/papers/2023-ocaml-eio). ## Specifications that can cross OS layers The specifications we want to express aren't confined to just one library. Consider a policy over a pipeline of a filesystem, a JSON parser and a network socket: > the agent may read files below `/data`; it may send to the network only values > derived from the `public` subtree of a parsed document; and no raw file bytes > should ever cross the socket. While multiple separate effect vocabularies are involved here, the property itself is a relation between them. Each layer contributes its own capability signature and its own specification monad; e.g. the filesystem's can borrow from an existing formal account of POSIX behaviour such as [SibylFS](https://anil.recoil.org/papers/2015-sosp-sibylfs), while the JSON parser is a pure relation between bytes and values. The composite policy can be assembled from them via monad transformers (details TBD!). Working out what a realistic information flow property looks like here is the first chunk of the project. ### Proof-producing extraction While the specification is written in Lean 4, it should be a DSL that can compile it into multiple artefacts: 1. proof obligations that can be discharged statically 2. a residual automaton in OxCaml for obligations that must be dynamically checked 3. a Lean proof that the second refines the first. Every trace the automaton accepts should satisfy the predicate transformer, and every trace that violates it should be rejected. Deciding where to cut between the static and dynamic halves will involve some difficult design choices, and so we'll ground this in a few practical interfaces such as a filesystem, a JSON parser, and a network interface. ## Implementing the automaton in Eio As a stretch goal, we'll embed this in OxCaml\! OCaml 5 [effect handlers](https://anil.recoil.org/papers/2017-ml-effects) are a much better interception point than anything that was available to me in 2005 in OCaml 3\! Each IO operation performed by an Eio fibre passes through a handler, so we could embed an automaton that can be ticked on each operation by the scheduler itself. OxCaml then earns its place on the fast path as it can be used to unbox and stack-allocate it so that a state transition is fast. Another good stretch goal would be to hand the specification writing to an LLM. Agents are [now plausible](https://anil.recoil.org/notes/fpl-launch) at producing mechanised Lean. ## Prerequisites Lean 4 and/or OCaml, or the appetite to learn both quickly. You will need interest in systems programming as well for the performance aspects. ## Background Reading - [Modularizing Reasoning about AI Capabilities via Abstract Dijkstra Monads](https://anil.recoil.org/papers/2024-hope-bastion), see the [slides](https://anil.recoil.org/slides/2024-hope-bastion-slides.pdf) and [Cyrus Omar](https://web.eecs.umich.edu/~comar/)'s [talk video](https://www.youtube.com/watch?v=U9H9xU-8-qc), and [why a sandbox](https://anil.recoil.org/notes/claude-copilot-sandbox) that is just a shell wrapper isn't sufficient. - [Dijkstra monads for free](https://doi.org/10.1145/3009837.3009878), Ahman et al, POPL 2017, and [Dijkstra monads for all](https://doi.org/10.1145/3341708), Maillard et al, ICFP 2019. - [Securing Verified IO Programs Against Unverified Code in Fstar](https://doi.org/10.1145/3632916), Andrici et al, POPL 2024. - [Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language](https://anil.recoil.org/papers/2009-icfem-spl) and [SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions](https://anil.recoil.org/papers/2005-spin-splat) for the historical work I did and [Creating High-Performance, Statically Type-Safe Network Applications](https://anil.recoil.org/papers/anil-phd-thesis) for the SSH/DNS server it was exercised on. - [Eio 1.0 – Effects-based IO for OCaml 5](https://anil.recoil.org/papers/2023-ocaml-eio) and [Effectively tackling the awkward squad](https://anil.recoil.org/papers/2017-ml-effects) for the Eio enforcement substrate, and [An io\_uring IO implementation for Lean](https://anil.recoil.org/ideas/lean-io-uring-backend) for a sibling project that puts Lean underneath the IO stack. Status: Available Level: MPhil Year: 2026 Project: OxCaml Labs Supervisors: Anil Madhavapeddy, Cyrus Omar ## Related - [Just a rumour of a bug is enough to find a security exploit these days](https://anil.recoil.org/notes/rumour-is-the-exploit) (note, 2026-08-22) - [The FP Launchpad takes off at IIT Madras](https://anil.recoil.org/notes/fpl-launch) (note, 2026-04-13) - [An io_uring IO implementation for Lean](https://anil.recoil.org/ideas/lean-io-uring-backend) (idea, 2026-04-01) - [Oh my Claude, we need agentic copilot sandboxing right now](https://anil.recoil.org/notes/claude-copilot-sandbox) (note, 2025-03-02) - [OxCaml Labs](https://anil.recoil.org/projects/oxcaml) (project, 2025-01-01) - [Modularizing Reasoning about AI Capabilities via Abstract Dijkstra Monads](https://anil.recoil.org/papers/2024-hope-bastion) (paper, 2024-09-01) - [Eio 1.0 – Effects-based IO for OCaml 5](https://anil.recoil.org/papers/2023-ocaml-eio) (paper, 2023-09-01) - [Effectively tackling the awkward squad](https://anil.recoil.org/papers/2017-ml-effects) (paper, 2017-09-01) - [SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems](https://anil.recoil.org/papers/2015-sosp-sibylfs) (paper, 2015-10-01) - [Creating High-Performance, Statically Type-Safe Network Applications](https://anil.recoil.org/papers/anil-phd-thesis) (paper, 2010-05-01) - [Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language](https://anil.recoil.org/papers/2009-icfem-spl) (paper, 2009-11-01) - [SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions](https://anil.recoil.org/papers/2005-spin-splat) (paper, 2005-08-01) --- Canonical: https://anil.recoil.org/ideas/lean-dijkstra-automata Type: idea Tags: lean, formal, ocaml, oxcaml, effects, ai