Z3-4Bio provides a unified semantic framework based on transition systems which allows translations from a range of formalisms and tools for modeling biological systems to SMT encodings usable within the Z3 solver. With Z3-4Bio, a set biological questions that are hard to study using simulation can be asked, and models can be analyzed formally against rich temporal specifications.