Lightweight Formal Verification in Real World, A Case Study