methods:
The OWR was specified in HOL with transcripts supplied in Z.
It was a hardware device, designed by ICL to meet the security requirement.
The design was formally proven against the security requirement using a specially modified version of Classic HOL.
This involved formal reasoning about information flow bandwidths.


modifying HOL:
HOL was modified, to make it more secure, and to permit loose constant specifications.
"new_axiom" and "mk_thm" were hidden from users.
Loose specifications were enabled by permitting the deletion of definitions, using a definition using the choice function, deriving a theorem of the form "x.P x P c" and then deleting the definition.


reals:
We had a look at implementing reals in HOL (this was 1988), using represention of real numbers as open downwardclosed cuts in prerationals represented as triples of natural numbers ((a,b,c) represents the rational ((ab)/(c+1)).
This was pretty heavy going (no linear arithmetic).
Long before we had the reals we had a way of talking about bandwidth without them, so we had to give up that little project and get on with the real work.

