* moved the grev formal correctness assertions into the module