I’ve been working on a Lean 4 formalization of the Correctness proof for the SFL algorithm. The complete proof is available at 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.