Verified by Lean

Every verdict of invariants comes with a certificate. yen checks it in Nix, and a checker written and proved in Lean 4 checks it again, outside Nix. The fleet and the rules are the ones of the invariants page, as working code:

{ yen, lib, ... }:
{
  yen.kinds.fleet = {
    spawns.host = _: yen.host;
    sinks.out.reduce = yen.lib.reduce.merge;
  };
  yen.kinds.host.fields = {
    addr = yen.lib.str;
    form = yen.lib.enum [
      "server"
      "laptop"
    ];
  };

  yen.fleet.main = { };
  yen.host.web = {
    addr = "10.0.0.1";
    form = "server";
  };
  yen.host.db = {
    addr = "10.0.0.2";
    form = "server";
  };
  yen.host.thinkpad = {
    addr = "10.0.0.50";
    form = "laptop";
  };
  yen.aspects.desktop.at = s: (s.form or null) == "laptop";
  yen.aspects.postgres.at = yen.host.db;
  yen.flake = { out, ... }: out;
}

# Rules by reference: a rule is a function of its variables, and its literals come from `yen.facts`:
# `host.form H "server"` is "H is a host whose form is server". A rule with `bad = H` that holds is a violation.
{ yen, ... }:
let
  inherit (yen.facts) host has lt;
in
{
  # no server runs a desktop
  yen.invariants.no-desktop-on-servers =
    { H }:
    {
      bad = H;
      pos = [
        (host.form H "server")
        (has yen.aspects.desktop H)
      ];
    };

  # no two hosts share an address: a rule across machines (`lt` keeps one of each pair)
  yen.invariants.unique-addr =
    {
      A,
      B,
      X,
    }:
    {
      bad = [
        A
        B
      ];
      pos = [
        (host.addr A X)
        (host.addr B X)
        (lt A B)
      ];
    };
}

To build the check, add the Lean battery to the flake outputs. nix flake check builds it only when the Lean checker verifies the verdict:

outputs =
  inputs:
  let
    result = inputs.yen.lib.eval {
      imports = [ (inputs.import-tree ./modules) ];
      inherit inputs;
      inherit (inputs.nixpkgs) lib;
    };
  in
  result.flake // {
    checks.x86_64-linux.lean = inputs.yen.lib.batteries.lean.verify {
      pkgs = inputs.nixpkgs.legacyPackages.x86_64-linux;
      inherit result;
    };
  };

lean.verify is the Lean battery. You need it only for a flake you write by hand. A flake from yen.lib.mkFlake with inputs.nixpkgs has this check already, as checks.<system>.yen-lean, for every fleet, clean or not. The docs build this check on this fleet in CI, and a second one that must be rejected: the fleet with mistakes.

The checker reads the rules as you wrote them, with their variables, the facts of the fleet, and the certificate. Lean does not trust the yen grounder. It grounds the rules over the facts itself and checks that its ground program covers the full one: every instance of a rule whose positive atoms can hold. Then it checks the certificate on it. This fleet gives the checker:

{
  facts = 23;
  proved = 0;
  refuted = 0;
  rules = 2;
}

This data is result.check.lean. What Lean proves, in lean/:

Theorem	Says
`sound` (Certificate.lean)	an accepted certificate is true in every interpretation closed under the well-founded operator of any ground program its rules cover
`not_both` (Certificate.lean)	no atom of an accepted certificate is both proved and refuted
`covers` (Ground.lean)	the program Lean grounds covers the full ground program of the rules and facts
`verify_sound` (Ground.lean)	on a verified verdict, every violation is false in every interpretation closed under the operator
`wfm_fixpoint`, `wfm_least` (Wfm.lean)	the well-founded model, defined in Lean, is the least fixpoint of the well-founded operator
`verify_wfm` (Wfm.lean)	on a verified verdict, every violation is false in the well-founded model of the full program
`shape_no_cycle` (Facts.lean)	on facts that pass the shape check, no scope is its own ancestor
`waves_respect`, `waves_acyclic` (Waves.lean)	verified deploy waves put every dependency in an earlier wave, so the graph has no cycle
`relevance` (Wfm.lean)	two programs with the same rules under a set of atoms give those atoms the same value: a change reaches only its cone

CI runs lean-check on every change: the proofs compile, and none uses sorry. The consistency of the well-founded model (no atom both true and false) is cited, from Van Gelder, Ross and Schlipf 1991, Theorem 5.4.

The checker also checks the shape of the facts: every id a fact names is a scope, each scope has one kind and at most one parent, and every scope reaches the root. Facts that fail are rejected before any rule is read.

Staged changes

Stage (yen.lib.stage) evaluates the fleet with a change and without it. Its lean field holds both verdicts, and yen-cert-check --change reads them: the staged verdict must verify, and the checker names the cone of the change, the atoms whose rules changed and every atom that reads them. By relevance, every atom outside the cone keeps its value. The MCP tool yen_stage answers with this check in lean, so an agent sees before it writes a file whether Lean accepts the change and which violations it can touch.

Deploy waves

lib.graphs.layers (see Graphs) orders a graph into waves: each node comes after everything it depends on. The battery lean.waves checks the waves in Lean. A cycle leaves nodes out of every wave, so the check fails and names them:

checks.x86_64-linux.waves = yen.lib.batteries.lean.waves {
  inherit pkgs;
  succ = { web = [ "db" ]; db = [ "net" ]; net = [ ]; };
};

Run the checker on any fleet without the battery: nix run github:vic/yen#yen-cert-check -- verdict.json, where verdict.json is builtins.toJSON result.check.lean. The MCP server gives the same check to agents as the tool yen_verify.

What stays trusted: Nix, which evaluates the fleet into facts (Lean checks only their shape), and the Lean kernel. An external relation decided by a Nix function (yen.relations.<name>.holds or .type) is not decided by Lean: the checker exits 2 on it. lt and neq are decided by Lean.

With the mistakes of the invariants page, a desktop on a server and a copied address, the check does not build:

# A desktop on a server, and a new host with a copied address.
{ yen, ... }:
{
  yen.aspects.desktop.at = yen.host.web;
  yen.host.spare = {
    addr = "10.0.0.2";
    form = "server";
  };
}

rejected: violations not refuted (2 rules, 30 facts, 32 ground rules, 6 proved, 0 refuted):
  ["bad", "no-desktop-on-servers", "fleet:main/host:web"]
  ["bad", "unique-addr", "fleet:main/host:db", "fleet:main/host:spare"]

Contribute Community Sponsor