Correctness infrastructure for the agentic era.
Built and operated for teams shipping agent-generated code.
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 is the practice that builds the missing layers.
layers 01–02, in production
$ nix eval github:kleisli-io/metaBuilder#examples.idl.validation idl = mb.ornaments.idl;
spec = idl.fromProtobuf {
name = "example-idl";
protos = [ ./schema.proto ];
languages = [ "cpp" "java" ];
};
program = mb.program.fromOrnamentedSpec
idl.IdlBuilder.T spec;{ diagnostics = [ ]; ok = true; }
source schema.proto tool protoc run protoc --cpp_out=$out/cpp schema.proto run protoc --java_out=$out/java schema.proto transform cpp (tree) transform java (tree) descriptor example-idl-idl materialize example-idl-generated (runCommand)
# example-idl-generated Builder: `runCommand` ## Inputs - source 'schema.proto' from ./schema.proto ## Tools - `protoc` ## Outputs - output 'cpp' at $out/cpp (tree) - output 'java' at $out/java (tree)
/nix/store/clb1z7fik1bzs1d1v5p7dalwmczdrvcm-example-idl-generated.drv
Live output. Every view above is the same spec, interpreted at nix eval time, before anything builds.
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.