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.
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;error: Type error at .interfaces[1].name: expected string, got int
2 error(s): .interfaces[1].name :: expected string, got int .interfaces[2].mtu :: expected int, got string
fail .interfaces[1].name : string fail .interfaces[2].mtu : int
$ nix eval --raw -f examples/handler-swap-validation.nix {strict|collecting|logging}examples/handler-swap-validation.nixOne 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.
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.
Built on the Kleisli stack. Operated from Tromsø.
An experiment report on metaBuilder, a typed builder DSL we built to test whether ornaments are what relate heterogeneous build descriptions, and what held under test once we did.
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.
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.