  Justification semantics plays a similar role in Modal Logic to that  played by Kleene realizability in Intuitionistic Logic. In both  cases, the intended semantics is existential: the  Brouwer-Heyting-Kolmogorov interpretation of Intuitionistic Logic  (Heyting 1934, Troelstra and van Dalen 1988, van Dalen 1986) and  Gödel’s provability reading of  \(\mathsf{S4}\) (Gödel 1933, Gödel 1938). In both  cases there is a possible-world semantics of  universal character which is a highly potent and  dominant technical tool. It does not, however, address the  existential character of the intended semantics. It took Kleene  realizability (Kleene 1945, Troelstra 1998) to reveal the  computational semantics of Intuitionistic Logic and the Logic of  Proofs to provide exact BHK semantics of proofs for Intuitionistic and Modal Logic.