In Robinson arithmetic $Q$ you can formulate the sentence $Con(Q)$ stating that $Q$ is coherent, but you cannot prove it, because Gödel's second incompleteness theorem also holds for $Q$: no consistent recursively axiomatized extension of $Q$ can prove its own consistency.
Actually, there exist self-verifying theories that are consistent first-order systems of arithmetic much weaker than $\textit{PA}$ (Peano arithmetic) and even $Q$, but that are capable of proving their own consistency. Dan Willard was the first to investigate their properties, and he has described a family of such systems. His idea is to formalise enough of the Gödel machinery to talk about provability internally without being able to formalise diagonalisation, to prevent Gödel's incompleteness theorems from applying to such formal systems.