  Building on previous work by Andr\'e Platzer, we present a formal language
for Stochastic Differential Dynamic Logic, and define its semantics, axioms and
inference rules. Compared to the previous effort, our account of the Stochastic
Differential Dynamic Logic follows closer to and is more compatible with the
traditional account of the regular Differential Dynamic Logic. We resolve an
issue with the well-definedness of the original work's semantics, while showing
how to make the logic more expressive by incorporating nondeterministic choice,
definite descriptions and differential terms. Definite descriptions necessitate
using a three-valued truth semantics. We also give the first Uniform
Substitution calculus for Stochastic Differential Dynamic Logic, making it more
practical to implement in proof assistants.
