We open-sourced lean4-markdown, a typed Lean 4 library for building Markdown documents programmatically. The idea is straightforward: if you're generating verification reports or audit traces in Lean 4, you want the document structure checked by the same type system as the rest of your code. Ill-formed Markdown becomes a type error rather than a runtime surprise. This is part of a small ecosystem we're building around Lean 4 as a general-purpose platform, alongside lean4-flow and lean4-json-schema. Happy to answer questions about design tradeoffs.