The current formalization models a single process executing Troupe’s intermediate representation under an information-flow monitor, with mailbox inputs and outputs. It establishes a knowledge-based security condition with separate bounds for downgrades.
The model has no thread creation or scheduler. The result concerns the modeled single-process semantics; it does not establish correctness of the full concurrent and distributed runtime or of the compiler.
The online report is transcribed from the Lean development using an LLM. The Lean development is the source of truth; the report connects definitions and lemmas to their Lean declarations.