newbie: apply TLA+ for DHT design?

[Han]

Hi,

I am working on a design and implementation of DHT (distributed hash table). As I am relatively new to DHT, I am thinking it's probably better to have spec validated before writing code. I went through TLA+ online course some time back, and now wondering if I should use TLA+ to write spec for DHT. I am refreshing my TLA+ knowledge and working on that myself, but wanted to check with the community to see   1) if that's a good idea,  2) if some existing literature about TLA+ for DHT validation I should read. (and would it be a too difficult task for a TLA+ newbie?)

Thanks in advance,

Han