I built the RealWorld app in Lean 4 leangineer.com

The author built a Medium-style RealWorld app entirely in Lean 4, including its Postgres-backed server and interactive website, and says it passes the project’s API and browser test suites. The backend is 1,033 lines; the post describes Lean-checked guarantees for route types, slug validity and HTML escaping, while noting the app was not derived from a formal specification and would need careful review before serving users.