The core idea of Separation Logic approaches is local reasoning. This is made possible by the formulation of “frame” rules that allow extending local reasoning to the entire heap after the axioms focus on the strictly necessary heap fragment. However, frame rules are often designed in an ad hoc way for a specific semantics, and there are cases where locality is hindered. Focusing on Incorrectness Separation Logic (ISL) we propose a theoretical characterization of axioms and a new frame rule by defining a calculational design of a semantic proof system for under-approximation, where the locality principle is justified in semantic terms. The proof system is parametric with the given semantics, and the applicability conditions are local for each command. We instantiate our semantic proof system with the ISL model semantics, thereby obtaining a novel logical system capable of deriving more triples than ISL. Our approach looks quite flexible and allows for language extensions.