In recent years, formal verification technology has received more and more attention, and it plays an important role in ensuring the safety and correctness of systems in critical areas of safety. As a branch of formal verification with a high degree of automation, model checking has a very broad development prospect. This work studies and proposes a new model checking technique, which can effectively check transition systems, including bug-finding and safety proof. Different from existing model checking algorithms, the proposed method, unsatisfied core (UC)-based approximate incremental reachability (UAIR), mainly utilizes the unsatisfied core to solve a series of candidate safety invariants until the final invariant is generated, so as to realize safety proof and bug-finding. In symbolic model checking based on the SAT solver, the UC obtained by the satisfiability solver is used to construct candidate safety invariant, and if the transition system itself is safe, the initial invariant obtained is only an approximation of the safety invariant. Then, while checking the safety, the candidate safety invariant is gradually improved until a real invariant is found that proves the system is safe; if the system is unsafe, the proposed method can finally find a counterexample to prove the system is unsafe. As a brand new method, UCs are exploited for safety model checking and sound results are achieved. As it is all known, there is no absolute best method in the field of model checking, although the proposed method cannot surpass the current mature methods such as IC3, CAR, etc., the method in this paper can solve 3 cases that other mature methods are unable to solve, it is believed that this method can be a valuable addition to the model checking toolset.