# A (somewhat) formally verified implementation of Markdown

**URL:** <https://talk.commonmark.org/t/a-somewhat-formally-verified-implementation-of-markdown/9108>\
**Category:** Uncategorized\
**Created:** [August 8, 2026, 7:47am UTC](https://talk.commonmark.org/t/a-somewhat-formally-verified-implementation-of-markdown/9108 "2026-08-08T07:47:17Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![paulbutcher](https://cdn.commonmark.org/user_avatar/talk.commonmark.org/paulbutcher/32/3500_2.png) [@paulbutcher](https://talk.commonmark.org/u/paulbutcher)\
**Post date:** [August 8, 2026, 7:47am UTC](https://talk.commonmark.org/t/a-somewhat-formally-verified-implementation-of-markdown/9108/1 "2026-08-08T07:47:17Z")

</div>

I’d like to announce [lean-markdown](https://github.com/paulbutcher/lean-markdown "https://github.com/paulbutcher/lean-markdown") a Lean implementation of both CommonMark and GitHub Flavored Markdown (GFM).

[A (somewhat) formally verified implementation of Markdown](https://paulbutcher.com/lean-markdown.html)

## **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.