Figure 2.10 on page 65:
\sigma(z) = z if z not in y1,...,yn

page 81: \phi(s(X),X) should be \phi(X,s(X))

Figure 3.9 on page 164: condition 8 should also require that F be a closed set, because the soundness proof requires F to have been reached before leaving the negation or its weak negation where the premise and antecedent apply. Thanks to Andrew Sogokon and Paul Jackson for identifying this bug. The antecedent of the conclusion of rule DV should also assume \chi. Thanks to Yong Kiam Tan for identifying this bug and sound generalizations of DV. The most comprehensive approach to ODE liveness is in:
Yong Kiam Tan and Andre Platzer. An axiomatic approach to existence and liveness for differential equations. Formal Aspects of Computing 33(4), pp. 461-518, 2021. DOI 10.1007/s00165-020-00525-0

The proof of rule DI'' in Proposition 3.2 on page 188 should explicitly say that \zeta=0 is impossible, so the mean-value theorem applicable, because \varphi(0) |= D(c)_x'^\theta > 0, which continues to hold on some open interval (0,k), because \varphi is continuously-differentiable and the differential term is continuously-differentiable as well by Lemma 3.1. Hence the infimum \zeta must be \zeta>=k>0. Thanks to Yong Kiam Tan for highlighting this.

Definition 4.3 on page 211: Case 2 should have a failure semantics (same as ?\chi in case 3) for states in which the evolution domain constraint \chi does not hold in the initial state. Thanks to Jean-Baptiste Jeannin for pointing this out.
http://www.cs.cmu.edu/~aplatzer/course/fcps14/16-difftemporal.pdf
DOI: 10.1007/978-3-319-08587-6_22