I’d like to announce lean-markdown a Lean implementation of both CommonMark and GitHub Flavored Markdown (GFM).
A (somewhat) formally verified implementation of Markdown
Guarantees
- Conformant: passes every test in the official CommonMark and cmark-gfm suites.
- Total: never panics or loops on any input, including adversarial input.
- Safe: proved to never let an AST leaf’s string content produce unescaped HTML markup, or break out of an attribute.
- Well-formed: for input with no embedded raw HTML, output is proved well-formed HTML.
Both CommonMark and GFM pass raw HTML through verbatim by design. For untrusted input use renderHtmlSafe which guarantees the output is both safe and well formed, including adversarial input.