Even though I first voted on "provers", I think it's worth distinguishing between ITPs and ATPs (interactive vs automated). The original proposal for this new SE site did not say it was for formal methods in general which may make the scope too broad. So that choice of name could be misleading unless we explicitly broaden the scope.
Quoting from QED survey (omitting obvious references for clarity), which I mentioned in my proposal:
1.2 Scope: Domain and Literature
We consider proof engineering research in the context of interactive
theorem provers (ITPs) or proof assistants (used interchangeably with
ITPs in this survey) that satisfy the de Bruijn criterion, which requires that
they produce proof objects that a small proof-checking kernel can verify;
the general workflow of such tools is illustrated in Figure 1.1. That is,
we consider proof assistants such as Coq, Isabelle/HOL, HOL
Light, and Agda; we do not consider program verifiers,
theorem provers, and constraint solvers such as Dafny,
ACL2, and Z3 except when contributions carryover.
This might be a good guiding principle for our future community as well. That is, ATPs like Z3 should not be hard off-topic, but the main focus should still be on proof assistants/ITPs.