A computing system that can’t lie to you.

Every action leaves a receipt. Money always adds up. Permissions never grow behind your back.

How? The rules are written as mathematics and checked by machine.

Fig. 01 The egg is whole. Something alive glows inside.

The idea

A glass box, not a black box.

Picture an AI that works for you. It earns money, spends money, and runs a small business. Every move drops a receipt that anyone can pick up and check.

You do not have to trust the AI, or the person running the machine. You check the record.

That is dregg. The glass is mathematics a computing system verifies. It can hold AI agents, files, money, votes, and games. Anything inside follows rules that cannot be quietly broken by an app, a hacker, or dregg’s builders.

One rule, three parts

The system protects the boundary.

A / the egg

The core

The operating system. Nothing touches your things without a key you handed out. Keys can be narrowed, never secretly widened.

B / the net

The cloud

What is served and what is billed both commit to the ledger. A key is your account; no ID is required.

In progress: the visitor-side checker that makes a lying host visible.

C / the orb

The engine

It exists. Its proofs caught twelve real bugs that testing missed.

Open evidence

Do not take the page’s word for it.

proven A receipt

A real object from the running system

Not a claim: an actual receipt, field by field, with the theorems a machine has checked about it. See what a verified action leaves behind →

re-runnable The proofs

Re-check every theorem yourself

The proofs ship in the repository. One command re-verifies them from scratch on your machine: the guarantee comes from the checker you run, not from us. The source →

from source Test network

Independent machines agreeing on history

A multi-node development network runs from the repository: independent machines agree and prove as they go. No public instance is up right now; a developer can start one from source. Not mainnet.

The builder

One engineer, with agents.

I’m ember, a systems and proof engineer. dregg brings together work across Rust before 1.0, protocol engineering at O(1) Labs, and seL4, the first operating system kernel with an end-to-end machine-checked correctness proof.

It was built with Claude, in agentic swarms. More about ember →