Building a verifier for sentences involving addition over the natural numbers
$\left(\mathbb{N},+\right)$ is a model of Presburger arithmetic. Persburger arithmetic is a complete theory (see the answer here), so for any model $\mathcal M$ for Presburger arithmetic (lets denote this theory by $T$) and every first order formula $\varphi$ in the language of $T$ it holds that:

$\mathcal{M}\vDash \varphi \iff T \vdash \varphi$

To see why this follows for completeness, assume $M\vDash \varphi$, then obviously $T\not\vdash \neg\varphi$, thus by completeness $T\vdash\varphi$ (the $\Leftarrow$ implication is trivial).

This shows you why your question reduces to finding a decision procedure for Presburger arithmetic. This has a known double-exponential lower bound, you can find a proof in Rabin and Fischer's paper "Super-Exponential Complexity of Presburger Arithmetic". This bound also holds for nondeterminstic algorithms.