You can use TLA+ -- it's what Amazon and Microsoft uses. TLA+ is a formal specification language, plain-old maths, and the tool suite includes a model checker and a pretty printer. The model checker verifies properties of your specification that you want to hold true such as liveness. And it also includes a pretty-printer for exporting your specifications into well-formatted PDF documentation. The nice thing about wr…
That's not true. TLA+ is very useful but only few services adopt and benefit from it. Also it's not very readable and cannot document many design aspects e.g. the reasons behind technical decisions.