This repository contains the implementation and formal proofs from our NFM2025 paper, showcasing the detailed work described in the publication. It includes code and verification processes to support reproducibility and further exploration of our results.