I spent two weekends building infra, an infrastructure-as-code tool in Lean 4. It does what Terraform does: you declare the resources you want, it reads what your cloud accounts actually contain, and it reconciles the difference. Three clouds, fourteen resource kinds, about 19,000 lines of Lean, 143 commits.