Abstract: 3-valued logic model checking is suitable for the reasoning based on higher-level abstract model.However,for 3-valued model checking algorithm,the witness and counterexample needs to be found.Therefore,3-valued model checking technology and the finding of witness and counterexample are explored in this paper.A set of 3-valued logic rules is proposed and a proof system is formed.This can be used to prove whether a model satisfies a property.The witness(counterexample) can be found for an existential(a universal) path quantifier during the proving procedure.The direction of a model refinement can be given by the achievement of witness and counterexample.Finally an example is given to explain the application of this proof system in the verification of digital logic designing.