I liked the layered approach in the IronFleet paper. IronFleet: Proving Practical Distributed Systems Correct https://www.microsoft.com/en-us/research/publica

I liked the layered approach in the IronFleet paper. IronFleet: Proving Practical Distributed Systems Correct https://www.microsoft.com/en-us/research/publication/ironfleet-proving-practical-distributed-systems-correct/ https://www.microsoft.com/en-us/research/publication/ironfle... It uses TLA for the distributed protocol part, and Hoare style verification for sequential code, which has excellent toolchain support.