Trellis
the human writes the spec; the agent writes the Soil
A specification layer, toolchain, and IDE for programs whose implementations are written by AI agents.
one file per definition
A function, type, or module header lives in its own .tr file; its generated .soil and its .lock sit beside it.
tests are the root of trust
Humans write the tests that gate lowering; the refinement checker is a ratchet, not the trust root; only the human sets accepted.
effects and capabilities
Effect rows on types; io is not ambient — functions take opaque capability values, and tests pass fakes.
content-addressed everything
Unison-style definition hashing makes checking incremental and caching exact.
What it is
Trellis is the human-facing layer: prose specifications, types, and tests, written in .tr files — Markdown with formal fenced blocks.
Soil is the target language it lowers to: a small, strict, refinement-typed ML with effect tracking — the assembly language of vibe-coding, designed to be easy for a machine to write and easy for a checker to verify, read by humans but rarely written by them.
The thesis
If an agent writes the implementations, the human-authored layer should consist of prose specifications, types, tests, and structural constraints. An agent lowers each definition to Soil under the supervision of a type checker, a refinement checker, and the tests; a per-definition lock file records the hashes, provenance, and trust status of everything.
Nothing that affects correctness exists only in an agent's context.