That is exactly the effort done in our group before (from TLA+ to real C++ implementation) - the challenge is that the gap between specification and the impleme

That is exactly the effort done in our group before (from TLA+ to real C++ implementation) - the challenge is that the gap between specification and the implementation is large in terms of both implementation details and language expressiveness. As a complementary approach, we have come up libraries for distributed system development with built-in implementation-level model checking support. You may check out https://github.com/Microsoft/rDSN https://github.com/Microsoft/rDSN for details.