L4 is a domain-specific specification language that facilitates semantically rigorous formalization of legal expressions found in legislation and contracts. In our talk we will demo the working pieces (as of late 2021 / early 2022): a low-level core and a high-level language, a transpiler to reasoning back-ends including static analysis / formal verification and an expert system web app, and a real-world case study.