Let $G = \langle A \mid R \rangle$ be a finitely presented group, given by a finite presentation. If $G$ is abelian, then we can verify this fact: simply verify the fact that $[a, b] = 1$ for all generators $a, b \in A$ (this can be done by enumerating all words equal to $1$ in the group). That is, the property "being abelian" is a semi-decidable property (however, the property of "being non-abelian" is not semi-decidable, by the Adian–Rabin theorem, cf. also this translation). I recently bumped into the following question(s), but couldn't figure out any obvious way to answer either:
Is the property of being solvable semi-decidable? Is the property of not being solvable semi-decidable?
That is, is it possible to verify that a group is solvable? Is it possible to verify that a group is not solvable? The same questions above can also be asked for solvability of bounded derived length; for example, can one verify whether $G$ is a metabelian group (i.e. derived length $\leq 2$)? For reference, nilpotency is semi-decidable, i.e. there is a procedure for verifying nilpotency, see the article "Verifying nilpotence" by Charles Sims.