Which is the correct universal enveloping algebra in positive characteristic?

The notions do indeed diverge in positive characteristic: there is the enveloping algebra, and then (in the case that $\mathfrak g$ is the Lie algebra of an algebraic group G) there is also the hyperalgebra of G, which is the divided-power version you mention. In characteristic 0 these two algebras coincide, but in positive characteristic they differ very much. In particular, the hyperalgebra is not finitely-generated in positive characteristic; see Takeuchi's paper "Generators and Relations for the Hyperalgebras of Reductive Groups" for the reductive case. There is also a good exploration of the hyperalgebra in Haboush's paper "Central Differential Operators of Split Semisimple Groups Over Fields of Positive Characteristic."

One can obtain the hyperalgebra as follows. I don't know in what generality the following construction holds, so let's say that $\mathfrak g$ is the Lie algebra of an algebraic group G defined over $\mathbb Z$. Then there is a $\mathbb Z$-form of the enveloping algebra of G (the Kostant $\mathbb Z$-form) formed by taking divided powers, and upon base change this algebra becomes the hyperalgebra. Alternatively, one can take an appropriate Hopf-algebra dual of the ring of functions on G (cf Jantzen's book "Representations of Algebraic Groups").

As for their uses, in positive characteristic the hyperalgebra of G captures the representation theory of G in the way that the enveloping algebra does in characteristic 0, i.e. the finite-dimensional representations of G are exactly the same as the finite-dimensional representations of the hyperalgebra. This fails completely for the enveloping algebra: instead, the enveloping algebra sees only the representations of the first Frobenius kernel of G.

This question popped up on the feed recently, and I wanted to add another, "brave new math"-style answer. Namely, the point of Lie algebras is that, in characteristic $0$, a Lie algebra (resp., an $L_\infty$-algebra) gives necessary and sufficient information to define a formal Lie group (resp., a cogroup object in CDGA). Global sections of this group form a commutative, co-associative Hopf algebra and the (topological/filtered/etc.) dual will be the universal enveloping algebra.

There is an analogous story to the $L_\infty$ story in characteristic $p$, proved by Akhil Mathew and Lukas Brantner, https://arxiv.org/abs/1904.07352. They prove that the structure of a derived connected formal group scheme (which determines a formal moduli problem) is determined by a so-called partition Lie algebra structure on the tangent space. This is no longer an "additive" structure (not determined by a multilinear operad unlike $L_\infty$), but it is "just" some nicely combinatorial algebraic structure on the tangent space. If you modify your definition of Lie algebra using this picture then to each (partition) Lie algebra you can associate a formal moduli problem, and to every formal moduli problem you can associate a universal enveloping algebra by taking the dual to a universal Hopf algebra associated to your formal moduli problem. From what I understand, the "$\pi_0$ operations" inherent in this structure are exactly Lie algebra operations and divided powers.

You forgot the third one: restricted enveloping algebra. Hence, in characteristic p we have 3 enveloping algebras with homomorphisms U->U_0->U_{dp} All 3 are Hopf algebras and can be used for different things. You need to formulate your question better. What do you want to use it for?

They are all different unless your Lie algebra is zero. If g is finite-dimensional, U is finitely generated but infinite-dimensional, U_0 is finite-dimensional and U_{dp} is not finitely-generated. If g is the Lie algebra of an algebraic group, you can describe U_{dp}(g) invariantly but you cannot really write generators and relations: U_{dp} is not finitely generated.