First order satisfiability that doesn't have finite models
Here's an amusing approach by Brock-Nannestad and Schürmann:

Truthful Monadic Abstractions

The idea is to try to translate first-order sentences into monadic first-order logic, by "forgetting" some of the arguments. Certainly the translation isn't complete: there are some consistent sentences which become inconsistent after translation.

However, monadic first order logic is decidable. One can therefore verify if the translation $\overline F$ of a formula $F$ is consistent:

$$ \overline F\not\vdash\bot$$

can be checked by a decision procedure, and implies

$$ F\not\vdash\bot$$

Which implies that $F$ has a model, by the completeness theorem.

This theme can apply somewhat more generally: identify a decidable sub-logic of your problem, then translate your problem into it, in a way that preserves truth. In particular modern SMT solvers like Z3 have gotten astonishingly good at proving satisfiability of formulas with quantifiers (by default $\Sigma^0_1$, but can perform well on $\Pi^0_2$ formulas).

Forcing seems to be far out of reach of automated methods at the present.