Model refinement is one of the main concepts which the Abstract State Machine (ASM) formal method is built on. The tool automatically checks refinement correctness by using an SMT representation of the ASM models.