The purpose of this talk is to introduce exploratory work in the development of a library offering composable, verified legal components written in Lean 4, a general purpose dependently typed programming language and interactive theorem prover. Our goal is to support computation, verification, and experimentation across a variety of legal fields, including civil procedure, securities law, property law, trusts and estates, tax law, and contracts.