add grev test and formal proof