What is proven
In a Lean 4 model, for every agent behaviour and every Cedar policy: nothing that may depend on another
tenant’s data reaches a tenant’s principals or tools (Model.isolation); data cannot lower or
launder a label (Model.no_launder); for a fixed schedule, what a tenant observes depends only on data it may read
(Model.noninterference); the executable monitor implements the model (Exec.refines);
an agent that depends only on its own tenant’s trusted data and calls only tenant-private tools is never denied
by the flow checks (Model.transparency).
Assumptions include a trusted session and tool registry, complete mediation, stateless tools and no side channels. The Python gateway and
the game’s monitor are tested against the Lean oracle, not proven. Nothing is claimed about Cedar itself.
Full list in the repository’s docs/spec.md.