There exist sentences of first-order logic that are satisfiable and are satisfiable only by models of infinite size. However, all such sentences I can think of are satisfied by infinite models that can be generated by a non-terminating algorithm of a finite size.
For a example, there exists a sentence of first-order logic that is satisfied only by a model of an infinite size:
$$ \exists x \lnot \exists y S ( y, x ) \land $$ $$ \forall x \exists y S ( x, y ) \land $$ $$ \forall x \forall y \forall z ( ( S ( x, z ) \land S ( y, z) ) \to x = y ) $$
A model for this sentence can be generated (listed, enumerated) by a finite algorithm that never terminates - just list the elements of the infinite model in a sequence one after another and make $S$ hold only for successive pairs of such elements.
Does there exist a sentence of first-order logic that is satisfiable only in some infinite models for which there does not exist a finite algorithm that generates them?