Decidability in groups

The problem whether $G$ is perfect, that is $G=[G,G]$ is decidable because you need to abelianize all relations (replace the operation by "+" in every relation) and solve a system of linear equations over $\mathbb Z$. For example, if the defining relations are $xy^{-1}xxy^5x^{-8}=1, x^{-3}y^{-2}xyx^5 = 1 $, then the Abelianization gives $-5x+4y=0, 3x-y=0$. Now you need to check if these two relations "kill" $\mathbb{Z^2}$. That means for some integers $a,b,c,d$ we should have $x = a(-5x+4y)+b(3x-y), y = c(-5x+4y)+d(3x-y) $. This gives 4 integer equations with four unknowns: $1=-5a+3b, 0=4a-b, 1=4c-d, 0=-5c+3d $. This systems does not have an integer solution (it implies $7a=1 $), so $G\ne [G,G]$.


Many of the undecidable properties of finitely presented groups are verifiable i.e. if they are true, then they can be proved true. Such properities include trivial, finite, abelian, nilpotent, free, automatic, hyperbolic, isomorphic to some other specified finitely presented group.

As a follow-up question, are there any properties of finitely presented groups that are known to be neither verifiable nor for there negation to be verifiable? Might solvability be such a property?