# Towards a formally verified implementation of the MimbleWimble cryptocurrency protocol

## TL;DR

This paper discusses the MimbleWimble cryptocurrency protocol's security and scalability, and proposes a model-driven verification approach to ensure the correctness of its implementation.

## Contribution

It introduces a formal verification method tailored for MimbleWimble, advancing the reliability of privacy-focused cryptocurrencies.

## Key findings

- Identified key security and scalability properties of MimbleWimble
- Outlined a model-driven verification framework for protocol correctness
- Discussed the potential for formal certification of implementations

## Abstract

MimbleWimble is a privacy-oriented cryptocurrency technology encompassing security and scalability properties that distinguish it from other protocols of the kind. In this paper we present and briefly discuss those properties and outline the basis of a model-driven verification approach to address the certification of the correctness of a particular implementation of the protocol.