We propose a deductive verification approach for proving functional correctness-i.e., partial-correctness and invariance properties-on transition-system models, and illustrate the approach by formally verifying a security hypervisor. Regarding partial correctness, we generalise the recently introduced formalism of Reachability Logic, currently used as a language-parametric logic for programs, to transition systems. We propose a coinductive proof system for the resulting logic, which can be seen as performing an infinite symbolic execution of the transition-system model under verification. We embed the proof system in the Coq proof assistant and formally prove its soundness and completeness. The soundness result provides us with a Coq-certified Reachability-Logic prover for transition-system models. The completeness result, although more theoretical in nature, also has a practical value, as it suggests a proof strategy that is able to deal with all valid formulas on a given transition system. Moreover , completeness enables us to add new sound inference rules to our proof system "for free", thereby making it more flexible and easier to use in practice. The complete proof strategy reduces partial-correctness verification to invari-ance verification; for the latter we propose an incremental technique for dealing with the case-explosion problem that is known to affect it. All these combined techniques were instrumental in enabling us to prove, within reasonable time and effort limits, that the nontrivial algorithm implemented in a security hypervisor that we designed in earlier work meets its expected functional requirements.