One notable feature of Isabelle is that it allows for the definition and in-built integrated support of alternative object logics via the interface of Isabelle/Pure in combination with Isabelle/Isar. While Isabelle is primarily known for its implementation of Isabelle/HOL, it offers several alternative object logics, such as Isabelle/ZF and Isabelle/HoTT.
The important part to note here is that most of the main functionality and many proof methods implemented in Isabelle (Pure) are readily available for any newly implemented alternative object logic.
It seems to me that most of the other proof assistants are (rigidly) aimed at a specific object logic (usually some variant of a dependent type-theory and its various extensions). While new axioms can usually be added, the definition of alternative object logics is rarely supported out-of-the-box (that is, without a substantial modification of the code base that requires knowledge that goes well beyond that of an average user of the proof assistant and possibly non-backward compatible changes).
The question is whether Isabelle is the only modular proof assistant in the aforementioned sense? Are there any emerging proof assistants that aim to provide a similar level of modularity? Are there any ongoing projects to introduce similar features into the existing popular proof assistants, such as Agda/Coq/Lean?