If you come from SQL

The mapping:

The surprise is that behaviour is in the language and checked before it runs. There is no query language: a view is an expression over the tables, and a rule is checked by the verifier in every sampled state, not by the database at commit time.

The first program you would write, departments and staff with a foreign key and a budget:

row Employee { id: id, name: string(64), dept: id, salary: money(2) }
row Dept { id: id, name: string(64), budget: money(2), payroll: money(2) }
unit Depts {
    caps storage;
    state depts: Dept[8];
    contract create(dept: id, name: string(64), budget: money(2)) {
        case budget <= 0 => fail BadBudget;
        else => Created: depts += [Dept { id: dept, name: name, budget: budget }];
        examples { {} (10, "Research", 1000000) => Created { depts: [Dept { id: 10, name: "Research", budget: 1000000 }] }; {} (10, "Research", 0) => BadBudget; }
    }
    // what the department can still spend; an absent department is Unknown
    contract room(dept: id) -> money(2) => Room(depts[dept].budget - depts[dept].payroll);
}
unit Staff {
    caps storage;
    state staff: Employee[32];
    contract hire(emp: id, name: string(64), dept: id, salary: money(2), room: money(2)) {
        case salary <= 0 => fail BadSalary;
        case salary > room => fail OverBudget;
        else => Hired: staff += [Employee { id: emp, name: name, dept: dept, salary: salary }];
        examples {
            {} (1, "Ada", 10, 500000, 1000000) => Hired { staff: [Employee { id: 1, name: "Ada", dept: 10, salary: 500000 }] };
            {} (1, "Ada", 10, 0, 1000000) => BadSalary;
            {} (1, "Ada", 10, 500000, 400000) => OverBudget;
        }
    }
}
// a computed column over the other table, kept by the compiler after every change
derived Depts.depts.payroll = for d => fold(e in where(x in Staff.staff: x.dept == d.id), acc = 0: acc + e.salary);
// the foreign key and the budget rule, as world invariants over both tables
invariant all(e in Staff.staff: any(d in Depts.depts: d.id == e.dept));
invariant all(d in Depts.depts: d.payroll <= d.budget);
flow create_dept(dept: id, name: string(64), budget: money(2)) atomic { Depts.create(dept, name, budget); }
// the department decides whether there is room (and whether it exists) before the hire is recorded
flow hire(emp: id, name: string(64), dept: id, salary: money(2)) atomic { let room = Depts.room(dept); Staff.hire(emp, name, dept, salary, room); }
view payroll(dept: id) = match lookup(Depts.depts, dept) { some d => some(d.payroll), none => none };
route POST "/depts" => create_dept(dept, name, budget);
route POST "/staff" => hire(emp, name, dept, salary);
route GET "/depts/{dept}/payroll" => payroll(dept);
scenario a_hire {
    create_dept(10, "Research", 1000000) => Created;
    hire(1, "Ada", 10, 500000) => Hired;
    hire(2, "Bob", 10, 600000) => OverBudget;
    hire(3, "Cy", 11, 100) => Unknown;
    payroll(10) => Value(some(500000));
}

scenario a_hire
  create_dept(10, "Research", 1000000) => Created
  hire(1, "Ada", 10, 500000) => Hired
  hire(2, "Bob", 10, 600000) => OverBudget
  hire(3, "Cy", 11, 100) => Unknown
  payroll(10) => Value(Some(500000))
  Depts = Depts { depts: [Dept { id: 10, name: "Research", budget: 1000000, payroll: 500000 }] }
  Staff = Staff { staff: [Employee { id: 1, name: "Ada", dept: 10, salary: 500000 }] }
5 step(s), all as expected

verify: 5 examples, 5 scenario steps and 6000 sampled checks passed

What the verifier taught while this program was written, in order. First, hire could reference a department that did not exist, because Staff cannot look into Depts: the foreign key is a world invariant, and the flow keeps it by asking Depts.room first, which fails Unknown for an absent department before anything is recorded. Second, payroll <= budget could break in two ways, a negative budget and a hire past the budget, so create refuses BadBudget and the flow carries the department’s remaining room into hire, which refuses OverBudget. Third, a view over a missing key panics, so payroll answers an option. Each of those is a state the verifier produced and showed.

Two honest notes for a SQL reader. payroll is a derived column because sum today takes an int column and a fold over money needs a typed context, which a derived column’s declared type gives and a view’s inferred type does not; that limit is recorded. And a stored program loads the units a flow touches, not the rows it needs, so tables of thousands of rows per tenant are fine and millions are not; the limits appendix has the numbers.