  MimbleWimble (MW) is a privacy-oriented cryptocurrency technology which
provides security and scalability properties that distinguish it from other
protocols of its kind. We present and discuss those properties and outline the
basis of a model-driven verification approach to address the certification of
the correctness of the protocol implementations. In particular, we propose an
idealized model that is key in the described verification process, and identify
and precisely state sufficient conditions for our model to ensure the
verification of relevant security properties of MW. Since MW is built on top of
a consensus protocol, we develop a Z specification of one such protocol and
present an excerpt of the $\{log\}$ prototype generated from the Z
specification. This $\{log\}$ prototype can be used as an executable model
where simulations can be run. This allows us to analyze the behavior of the
protocol without having to implement it in a low level programming language.
Finally, we analyze the Grin and Beam implementations of MW in their current
state of development.
