Aah thank you on both counts yes. One interesting feature he told me about is they wrote a "reverse compiler" that would take Spark code and turn it into the associated formal (Z) spec so they could compare that to the actual Z spec to prove they were the same. Kind of nifty.
