kleisli.io

Correctness infrastructure for the agentic era.

Formal methods, type theory, Nix.

The verification layer is missing. Agents generate code faster than any human process can check it. The bottleneck is not skill. It is architecture. Kleisli.IO builds the missing layers.

The verification layer.

  Pos = refined "Pos" Int (x: x > 0);
  Network = Record {
    hostName = String;
    port = Pos;
    interfaces = ListOf (Record { name = String; mtu = Pos; });
  };

  badConfig = {
    hostName = "kleisli.io";
    port = (-1);
    interfaces = [
      { name = "eth0"; mtu = (-50); }
      { name = 42;     mtu = 1500; }
      { name = "eth2"; mtu = "big"; }
    ];
  };

  comp = Network.validate badConfig;
  runWith = handlers: state: fx.handle { inherit handlers state; } comp;
strict
error: Type error at interfaces.[0].mtu: expected Pos, got int
collecting
4 error(s):
  interfaces.[0].mtu :: expected Pos, got int
  interfaces.[1].name :: expected String, got int
  interfaces.[2].mtu :: expected Pos, got string
  port :: expected Pos, got int
logging
  pass  hostName : String
  fail  interfaces.[0].mtu : Pos
  pass  interfaces.[0].name : String
  pass  interfaces.[1].mtu : Pos
  fail  interfaces.[1].name : String
  fail  interfaces.[2].mtu : Pos
  pass  interfaces.[2].name : String
  fail  port : Pos
$ nix eval --raw -f examples/handler-swap-validation.nix {strict|collecting|logging}examples/handler-swap-validation.nix

One computation. Three handlers. Three semantics. The specification defines what to check; the handler decides how to respond. evalModules bakes halt-on-first into the module system (nixpkgs#367882); swapping it requires forking nixpkgs.

nix-effects on GitHubDependent Types in Pure Nix

The coordination layer.

kli is the coordination layer. An append-only event log is the specification; a projection is the handler. Privacy redaction, CRDT merges, retention windows — all are handlers over the same log. No central coordinator, because the log doesn't need to know who's reading.

Agent Coordination Is a Distributed Systems Problem
09:14task.createrotate-mesh-credentials
09:14session.joinagent-a
09:16observation12 WireGuard peers regenerated
09:18session.joinagent-b
09:20observationall WireGuardPeers pass under strict handler
09:21tool.calldeploy push 5 machines
09:22observationmesh converged, no runtime coordinator
09:23session.leaveagent-b (graceful)
in production

Kleisli.IO operates the complete technical infrastructure for the Lie-Størmer Center, Norway's national center for mathematics.

Built on the Kleisli stack. Operated from Tromsø.

Lie-Størmer-senteretUiT The Arctic University of NorwayAMTI

Going deeper.

nixFebruary 2026

Dependent Types in Pure Nix

nix-effects embeds a Martin-Löf Type Theory proof checker in pure Nix. Dependent functions, dependent pairs, identity types with J, cumulative universes, verified extraction of plain Nix functions from proof terms. The whole system runs at nix eval time.

nixFebruary 2026

Trampolining Nix with genericClosure

Nix has no loops and no tail-call optimization. builtins.genericClosure, the package dependency primitive, doubles as a general-purpose trampoline once you break the thunk chain.

event-sourcingFebruary 2026

Agent Coordination Is a Distributed Systems Problem

AI agent sessions are distributed processes: private state, independent failure, concurrent access to shared resources. Event sourcing gives sessions durable history; CRDTs give them convergent merge, with correctness guarantees that are purely algebraic, requiring no network model.

Agents write code.
Your team needs to know it is correct.

contact@kleisli.iogithub.com/kleisli-io