Ist this formally verified by any chance ? I feel like there's space where formal designs could be expressed in TLA+ such that its easier for the community to keep track of the design.