Skip to content
{yen}

Check a fleet you already have

You do not have to move your machines to Yen to get its checks. Yen is about the model of your fleet: which hosts you have, where they live, and how they relate to each other. That model can sit next to the flake you already have, while every host keeps being built by the same nixosConfigurations as today. Yen reads the model, decides your rules on it, and gives you one flake check. Nothing else in your flake changes.

I still think you will want to configure your hosts with Yen one day, because then the model and the machines can never disagree. But you can start with the check, and move hosts over later, one at a time or never.

The model

Section titled “The model”

The model is plain data. Each host has an address, a region, and the host it uses as its database. Regions and hosts are both part of the fleet, so a host points at its region by reference, and a typo is an error instead of a new region nobody meant to create:

modules/model.nix
# The fleet as data: where each host lives, its address, and the database it talks to. Nothing here configures a
# machine. Your hosts stay built the way they are built today.
{ yen, ... }:
{
  yen.kinds.fleet.spawns = {
    region = _: yen.region;
    host = _: yen.host;
  };
  yen.kinds.region = { };
  yen.kinds.host.fields = {
    addr = yen.lib.str;
    region = yen.kinds.region;
    db = yen.lib.maybe yen.kinds.host;
  };


  yen.fleet.main = { };
  yen.region.eu = { };
  yen.region.us = { };
  yen.host.db = {
    addr = "10.0.0.2";
    region = yen.region.eu;
  };
  yen.host.api = {
    addr = "10.0.0.1";
    region = yen.region.eu;
    db = yen.host.db;
  };
  yen.host.backup = {
    addr = "10.0.1.1";
    region = yen.region.us;
  };
}

The rules

Section titled “The rules”

A rule is a mistake you never want to deploy, written once for the whole fleet. These two are the classic ones that each host passes alone: two hosts with the same address, and a database in another region than the host that talks to it.

modules/rules.nix
# Two rules across machines. Each one is a mistake that no single host can see on its own.
{ yen, ... }:
let
  inherit (yen.facts) host lt;
in
{
  # no two hosts share an address (`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)
      ];
    };


  # a host and its database live in the same region
  yen.invariants.db-same-region =
    {
      H,
      D,
      R,
    }:
    {
      bad = H;
      pos = [
        (host.db H D)
        (host.region H R)
      ];
      neg = [ (host.region D R) ];
    };
}

One output

Section titled “One output”

The flake adds checks and nothing more. Merge it into the outputs you already have:

flake.nix
{
  description = "yen: check the model of a fleet you already have";


  # the outputs you have stay as they are (nixosConfigurations, packages, ...); yen adds only its check
  outputs = inputs: {
    inherit
      (inputs.yen.lib.mkFlake {
        inherit inputs;
        inherit (inputs.nixpkgs) lib;
      } (inputs.import-tree ./modules))
      checks
      ;
  };


  inputs = {
    yen.url = "github:vic/yen";
    import-tree.url = "github:denful/import-tree";
    nixpkgs.url = "https://nixos.org/channels/nixos-25.05/nixexprs.tar.xz";
  };
}

With inputs.nixpkgs, the check is checks.<system>.yen-lean. It runs the Lean checker on the verdict, so it builds only when no rule is broken, no rule is left undecided, and the proof checks. You run it the way you run any check, locally or in CI:

Terminal window
nix flake check

This fleet is clean: no violations, and no errors.

result
{
  errors = [ ];
  violations = [ ];
}

A plausible mistake

Section titled “A plausible mistake”

Someone adds a host web by copying api, and moves it to us. The new host still has the address of api, and its database is still in eu. Both hosts evaluate fine, and both of these would reach production:

variants/clone.nix
# A plausible edit: a new host `web`, copied from `api` and moved to `us`. It keeps the address of `api`, and its
# database is still in `eu`.
{ yen, ... }:
{
  yen.host.web = {
    addr = "10.0.0.1";
    region = yen.region.us;
    db = yen.host.db;
  };
}

With this edit, the check fails and names each machine and each rule it breaks:

result
{
  errors = [ ];
  violations = [
    [
      "bad"
      "db-same-region"
      "fleet:main/host:web"
    ]
    [
      "bad"
      "unique-addr"
      "fleet:main/host:api"
      "fleet:main/host:web"
    ]
  ];
}

Yen checks the model you write, not the machines you build. When the two can drift apart, keep the model honest by reviewing it with the hosts it describes, or move those hosts to Yen so the model is what builds them. The invariants page has more about rules, and From a flake shows the move.

ContributeCommunitySponsor