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.
Kleisli.IO builds nix-effects. Infrastructure validation as algebraic effects, in pure Nix. Every constraint is a suspended effect. Three handlers, same validation logic.
Peers = ListOf (refined "WireGuardPeer" Attrs
(p: p ? publicKey && p ? endpoint));
validate Peers [
{ publicKey = "dGVz..."; endpoint = "10.0.0.1:51820"; }
{ endpoint = "10.0.0.2:51820"; }
];error in Peers[1]: missing publicKey2 violations: Peers[1] missing publicKeypass Peers[0] fail Peers[1]Kleisli.IO builds kli. Append-only event logs, conflict-free replicated state, no central coordinator.
Built on the Kleisli stack. Operated from Tromsø.
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.
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.