The notion of model of intuitionistic propositional logic (IPL) I'm
most familiar with (being a category theory/PL nerd) is a Heyting
algebra (HA): a poset with finite meets, finite joins and a Heyting
implication. If you add propositional variables, the model includes a
choice of how to interpret them as elements of the HA and if you
include axioms, their interpretation must be true in the HA.

Then you can interpret every proposition of IPL as an element of the
HA where you interpret conjunctions as meets, disjunctions as joins
and implication as the Heyting implication. If G |- A is provable then
/\ [G] |- [A] is true.

If you look up what a model of IPL is though, you'll likely find
Kripke models, and they look at first a bit different: It's a pair of
a poset W, and a "forcing relation" ||- between elements of W and
propositions of IPL satisfying a bunch of properties:

1. for variables x, if w ||- x and v <= w then v ||- x
2. w ||- p /\ q iff w ||- p and w ||- q
3. w ||- true is true
4. w ||- p \/ q iff w ||- p or w ||- q
5. w ||- false is false
6. w ||- p => q iff for any v <= w if v ||- p then v ||- q

Despite the cosmetic difference, Kripke models are instances of the HA
model construction. Given a poset W, the HA in question is
Prop^(W^op), the poset of antitone functions from W to Prop
(classically, Prop is just the boolean order 0 <= 1). This has the
pointwise ordering: f <= g if for every w. f w implies g w.

This is a Heyting Algebra:

top w iff true
(f /\ g) w iff f w and g w
bot w iff false
(f \/ g) w iff f w or g w
(f => g) w iff for any v <= w. if f w then g w

Then an interpretation of the propositional variables in this HA would
be an assignment for each variable X and w a proposition [x] w that is
antitone in w: if [x] w and v <= w then [x] v. Then the model HA
interpretation defines exactly our Kripke forcing semantics. It
defines for each proposition of IPL p a function from W to Prop that
is antitone, i.e., [p] : W^op -> Prop. Then the definition of Kripke
model is just an infix notation for this semantics:

w ||- p := [p] w

And if you unravel the definitions of the HA semantics and the HA
structure of the poset, you reproduce exactly the definition of a
Kripke model.

Bonus: this is all a "de-categorification" of a similar situation for
lambda calculus. The Kripke models are presheaf categories and the HA
are bi-cartesian closed categories.