I'd start by reading the papers mentioned below and then implementing a real distributed kv store without any fluff, just hard code your test cases into a simple client. Then try load testing by running a ton of your client. The problems you run into will be practical and real and you will have to debug them yourself with real tools. Then after that basic exercise I think Maelstrom will be more useful to you. TLA+ is an awesome design tool but imo implementation practice is more helpful for a beginner, you'll be more familiar with the problems TLA+ can help you solve.

https://omscs.gatech.edu/cs-6210-advanced-operating-systems