Dregg is a distributed object-capability operating system whose kernel is written and formally verified in Lean 4. The verified Lean function serves as the actual executor rather than a model of the system. It models the entire machine including desktop, database, and distributed swarm using a language of cells, turns, and capabilities. State changes require unforgeable capabilities and produce verifiable receipts.