How formal verification was used to prove that a Resource Allocator Unit correctly processed any combination and sequence of input requests to allocate, update or release resources.