Comment by dboreham

If only TLA+ could work with the actual product code, or even some machine-translation of same.