``The treatment should be written and well commented using TLA+ to give everyone a common ground: math.''

100% agreed.

Then developers, once you get them, can read this and start working at once: would be clear what is desired.

For those who don't already know, there's a Java program that can test TLA+ code, run cases and display output. It can mechanically check model work.