Hybrid verification integrating HOL theorem proving with MDG model checking