  We introduce the $\Sigma_1$-definable universal finite sequence and prove
that it exhibits the universal extension property amongst the countable models
of set theory under end-extension. That is, (i) the sequence is
$\Sigma_1$-definable and provably finite; (ii) the sequence is empty in
transitive models; and (iii) if $M$ is a countable model of set theory in which
the sequence is $s$ and $t$ is any finite extension of $s$ in this model, then
there is an end-extension of $M$ to a model in which the sequence is $t$. Our
proof method grows out of a new infinitary-logic-free proof of the Barwise
extension theorem, by which any countable model of set theory is end-extended
to a model of $V=L$ or indeed any theory true in a suitable submodel of the
original model. The main theorem settles the modal logic of end-extensional
potentialism, showing that the potentialist validities of the models of set
theory under end-extensions are exactly the assertions of S4. Finally, we
introduce the end-extensional maximality principle, which asserts that every
possibly necessary sentence is already true, and show that every countable
model extends to a model satisfying it.
