Great! Now I just have to mechanically convert it to TLA+ and the verification results are hopefully exploitable business ideas.