# Spanning-forest cluster linearization

**URL:** <https://delvingbitcoin.org/t/spanning-forest-cluster-linearization/1419>\
**Category:** Implementation\
**Tags:** mempool\
**Created:** [February 4, 2025, 2:31pm UTC](https://delvingbitcoin.org/t/spanning-forest-cluster-linearization/1419 "2025-02-04T14:31:21Z")\
**Posts on this page:** 1\
**Showing post:** 13

<div class="post-metadata">

**Author:** ![isadofschi](https://delvingbitcoin.org/user_avatar/delvingbitcoin.org/isadofschi/32/1928_2.png) [@isadofschi](https://delvingbitcoin.org/u/isadofschi)\
**Post date:** [April 16, 2026, 4:02pm UTC](https://delvingbitcoin.org/t/spanning-forest-cluster-linearization/1419/13 "2026-04-16T16:02:02Z")

</div>

I’ve been working on a Lean 4 formalization of the [Correctness proof](https://delvingbitcoin.org/t/spanning-forest-cluster-linearization/1419#p-4171-h-21-correctness-7) for the SFL algorithm. The complete proof is available at [isadofschi/cluster-mempool-formalization](https://github.com/isadofschi/cluster-mempool-formalization).

Some parts of the Cluster mempool definitions & theory thread (such as feerate diagrams) are also formalized as part of the proof.

---

_[View the full topic](https://delvingbitcoin.org/t/spanning-forest-cluster-linearization/1419)._