As an efficient scheduling method, the intelligent planning of ammunition support operation of carrier-borne air craft is an important way to boost the development of advanced technology of aircraft carrier engineering. Ensuring the correctness of operation planning schemes under the high safety-critical attribute has gradually become the key technical bottleneck restricting the security of their practical application deployments. Aiming at the challenges posed by the difficulties in modeling ammunition support systems, describing operation execution behavior, and realizing formal verification tools, this study proposes a behavior model for ammunition support systems based on the separation logic idea, where the theorem prover Coq is employed to conduct formal verification on the operation planning scheme. First, a serialized two-tier resource heap model that conforms to the characteristics of ammunition support operation is proposed. Subsequently, a set of modeling language and operational semantics are constructed based on this model to describe job execution behavior. Finally, a proof assistant tool is implemented in Coq. The usability and engineering practicability of the tool are verified by interactive demonstrations of several typical ammunition support operation planning schemes.