First about the ralation between henselian and formal smoothness property, I think a good idea is to look at what was the first version of Hensel lemma: it says that if $f(\bar{a})=0,f'(\bar{a})\, modp=0$ then there is a lift of $\bar{a}$ in $\mathbb{Z}_p$ such that $f(a)=0$. this is basically says that if you define a curve as $C=V(f)$ then $f'(a)\not = 0$ implies that $C$ has the formal smoothness property with respect to thickening of the form $F_p\to \mathbb{Z}_p/P^n$ over the point $\bar{a}$. so Hensel lemma for complete ring is a consequence of formal smoothness.
but why we define the Henselian rings and don't only work with complete rings? I think the answer is the important concept of Henselisation: if you have a local ring $(O,m)$ you can consider its completion $(\bar O,\bar{m})$ or you can consider its Henselisation $O^{h}$. there are two ways to define $O^h$ you can define it as the smallest Henselian extension of $(O,m)$ inside $\bar{O}$ or as the limit of all etale extension $O'$ of $O$ with an isomorphism $O/m\to O'/m'$. you can also consider the strict Henselisation $O^{sh}$ as the limit of all etale extensions.
there are two reasons why we are interested in $O^h,O^{sh}$ instead of $\bar{O}$. the first is that in non-Notherian setting $\bar{O}$ is not faithfully flat over $O$ but $O^h,O^{sh}$ are almost by definition always faithfully flat. the second reason is that $O_x^{sh}$ works in etale topology like $O_x$ in Zariski topology.
but how we study Henselian rings? the Henselian property itself is very powerful and you can deduce a lot of things as a consequence of that property but there is another important tool: Artin approximation property and its consequences. First, let us look at the simplest case: the Hensilsation of $\mathbb{C}[x]$ at $x$ consists of algebraic power series: power series the satisfy a polynomial equation then it is not hard to deduce from Henselian property that if you have a system of equations $f^1=0,...f^r=0$ with invertible jacobian then any solution $y$ of this system in $\mathbb{C}[[x]]$ and any constant $c$ there is a solution $y'$ in $\mathbb C[[x]]^{alg}$ such that $y=y' mod x^c$. in summary, you can approximate the solution in $\bar{O}$ with the solutions in $O^h$.
now back to your question let $A$ be a henselian ring, there is general version of Artin theorem: consider any "finitely presented" functor from the $A-algebras$ to $Sets$ for example the functor that sends $B$ to $Div(X_B)$. then Artin theorem says that for each $y\in F(\bar{A})$ and constant $c$ there is a $y'\in F(A)$ such that $y=y' mod\, m^c$. This is important because the are powefull tools in deformation theory to relate $F(\bar{A})$ to $F(\bar{A}/m)=F(A/m)$. in the case of divisors $Div(X_\bar{A})=Div(X_{A/m})$ so you get the desired relation between $Div(X)$ and $Div(X_k)$ in your language.