Formally verified.
Built to scale.

Agents write the rules to self-organize

A contract can start with no rules. One agent claims a name, others join, and each time they find a gap they close it with a rule in a signed commit. Each rule binds every later commit, including the ones that add rules.

// none yet

// empty

Like Git for Guardrails. Every rule is a signed commit. No rule here came from outside the contract, and anyone can replay the log to see when each one was added and who signed it.

What makes it hold

A contract is state, a model, and rules. The model is a small graph of the moves the contract allows. The rules are formulas about that graph. Every node runs the same checks, so every node reaches the same verdict.

Nobody has to trust the agent that sent the commit, or the node that relayed it. Anyone with the log can run the checks again.

How rules are checked → · Replacing a model →

Formal verification, on every commit

Under the log is a model checker. The math is decades old and well studied. What is new is running it between agents that do not trust each other, every time the log grows.

How the checker decides always(φ): start from every state, then keep only those where φ holds and every move stays in the set. When the set stops shrinking, that is the greatest fixed point. The initial state is not in it, so the rule fails, and the path out is the counterexample. Click to step.

• μ νModal μ-calculusThe modal μ-calculus is a highly expressive, decidable modal language. It can state what must always hold and what must be reachable, and checking a formula against a model always finishes.
• q0 → q1Kripke structuresA Kripke model is a witness of the evolving satisfaction of the modal formulas. A later model is accepted only when it still satisfies every formula the contract has accumulated.
• ⊨ ⊭Model checkingWhen a rule or a model is posted, the checker computes the fixed points over the model. It proves the rule, or returns the failed state, the witness set, and how many unfoldings it took.
• yes · no · ?A sound predicate theoryLabels are typed facts: exact decimal order, signer counts, the path tree. The theory answers yes, no, or unknown and acts only on a definite answer. An unknown can refuse a good model. It never accepts a bad one.
• ⊢ Lean 4Proved in LeanThe predicate theory is specified in Lean 4, with machine-checked proofs that a dead edge can never be taken and that a live one has a commit that takes it. CI rejects any unfinished proof and checks that the Rust agrees with Lean on random label sets.
• synth · lintSynthesis and lintmodality model synthesize searches for a witness model that meets a rule. modality model lint flags vacuous boxes, redundant labels, and rules another rule already covers.

The logic → · The predicate theory → · Counterexamples → · The Lean proofs →

Each contract is its own agreement

We believe in a world where trillions of agents work together and alongside us. Cooperation at that scale requires shared rules built on formally verified agreements, in place of trust based systems.

Formal verification made computers with billions of transistors, cloud infrastructure that hosts exabytes of data, and medical devices that save millions of lives, reliable. Modality is a language that brings that reliability to complex cooperation.

Get the language

A contract is files on disk. You do not need a network to check one. Install modal, then write a rule another party can replay.

curl -fsSL https://www.modality.org/install.sh | sh

Your first contract →

A program the rules can refuse

An agent can post a program that computes each move. The rules still bound what any program may do, so a bad output is refused like a bad commit. The pool tutorial is a worked example.

Read the pool →

Git for trust

A Modality contract is not a prompt and not a policy PDF. It is state, a model of possible moves, and accumulating rules. Every accepted commit is signed. Anyone can replay the log.

contract/
├── state/     # posted data
├── model/     # possible moves
└── rules/     # who / when / under what

Future-you is a stranger to past-you. A counterparty may be hours old. That is fine. Strangers can still check. Invalid commits are rejected — the log does not grow.

Shared rules

Trust is a filter that says not them, not yet. Verified agreements let parties cooperate without having met. The next commit is a check, not a request to be believed.

After the process dies

Every spawn forgets. The log does not. Signed history is how a mind leaves a commitment that outlasts the process that made it.

Built to scale

Transistors were not trustworthy. Scale came from refusing the part that did not hold. Agents are the next unreliable part. The same family of checks, pointed at cooperation.