pith. sign in

arxiv: 1907.01688 · v1 · pith:REZTQBYEnew · submitted 2019-07-03 · 💻 cs.CR

Towards a formally verified implementation of the MimbleWimble cryptocurrency protocol

Gustavo Betarte , Maximiliano Cristi\'a , Carlos Luna , Adri\'an Silveira , Dante Zanarini This is my paper

Pith reviewed 2026-05-25 10:50 UTC · model grok-4.3

classification 💻 cs.CR
keywords MimbleWimblecryptocurrency protocolformal verificationmodel-driven approachprivacy propertiesscalabilityimplementation correctness
0
0 comments X

The pith

A model-driven verification approach can certify the correctness of a MimbleWimble implementation.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents the security and scalability properties that distinguish MimbleWimble from other cryptocurrency protocols. It then outlines the basis for using models to verify that a concrete implementation satisfies those properties. A sympathetic reader would care because formal certification could establish that an implementation preserves privacy and scalability guarantees without hidden flaws. The approach relies on models that remain faithful to the protocol while supporting automated or semi-automated checking.

Core claim

The paper claims that a model-driven verification approach addresses the certification of the correctness of a particular implementation of the MimbleWimble protocol by capturing its distinguishing security and scalability properties in models that support verification.

What carries the argument

The model-driven verification approach that captures protocol properties in models amenable to automated or semi-automated checking.

If this is right

  • The implementation can receive a formal certificate of correctness with respect to the modeled properties.
  • Verification can proceed without requiring exhaustive manual proof for every detail.
  • The same modeling technique could apply to other privacy-oriented cryptocurrency protocols.
  • Scalability claims can be checked alongside security properties in the same framework.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the models succeed, they could serve as a reusable template for verifying updates or variants of the protocol.
  • The approach might reduce reliance on informal audits by shifting effort to model construction and checking.
  • Neighboring problems such as verifying mixing protocols or other blockchain privacy layers could adopt similar model structures.

Load-bearing premise

The security and scalability properties of MimbleWimble can be captured in models that are both faithful to the protocol and amenable to automated or semi-automated verification without prohibitive effort or loss of fidelity.

What would settle it

A concrete modeling attempt that either deviates from the protocol's actual behavior or requires prohibitive manual effort to verify would show the approach does not work as claimed.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper presents the security and scalability properties of the MimbleWimble protocol and outlines a model-driven verification approach intended to certify the correctness of a particular implementation of the protocol.

Significance. If concrete models and proofs were supplied, the work could contribute to the application of formal methods in cryptocurrency protocol verification, particularly for privacy and scalability properties that are difficult to assess informally.

major comments (2)
  1. [Verification Approach] The verification approach section provides only a high-level sketch of a model-driven strategy without any formalized properties, example models of core components (such as transaction kernels, range proofs, or cut-through), or tool-specific encodings; this leaves the central practicality assumption—that the protocol properties can be captured faithfully yet tractably for automated verification—unexamined and untestable.
  2. [Properties of MimbleWimble] The properties section discusses security and scalability at a conceptual level but supplies no formal specifications or definitions that could serve as the starting point for the proposed verification; without these, it is not possible to evaluate whether the outlined approach addresses the protocol's distinguishing features.
minor comments (1)
  1. [Abstract] The abstract and introduction could more explicitly frame the contribution as a high-level proposal rather than implying a completed outline with sufficient detail for certification.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments. The manuscript is explicitly positioned as an outline of properties and a high-level verification strategy (see title and abstract), not a complete formalization. We address each major comment below, maintaining the paper's intended scope.

read point-by-point responses

  1. Referee: [Verification Approach] The verification approach section provides only a high-level sketch of a model-driven strategy without any formalized properties, example models of core components (such as transaction kernels, range proofs, or cut-through), or tool-specific encodings; this leaves the central practicality assumption—that the protocol properties can be captured faithfully yet tractably for automated verification—unexamined and untestable.

    Authors: The manuscript does not claim to supply formalized properties, example models, or tool encodings; its abstract states that it 'outlines the basis' of the approach. The practicality argument rests on the protocol's modular structure (e.g., kernel-based transactions and cut-through), which is discussed conceptually to indicate why model-driven methods are promising. No revision is needed, as adding full models would exceed the paper's stated purpose as a preliminary outline. revision: no

  2. Referee: [Properties of MimbleWimble] The properties section discusses security and scalability at a conceptual level but supplies no formal specifications or definitions that could serve as the starting point for the proposed verification; without these, it is not possible to evaluate whether the outlined approach addresses the protocol's distinguishing features.

    Authors: The properties are presented at a conceptual level to identify MimbleWimble's distinguishing security and scalability characteristics and thereby motivate the verification effort. The paper makes no assertion that it supplies formal specifications; those would be developed as part of subsequent verification work. The outlined approach is therefore evaluated against the conceptual properties as described. No revision is required. revision: no

Circularity Check

0 steps flagged

No circularity; high-level proposal with no derivations or equations

full rationale

The manuscript is an outline of a model-driven verification approach for MimbleWimble. It discusses properties at a high level and sketches a general verification strategy but presents no equations, no formalized models, no fitted parameters, and no predictions. No derivation chain exists that could reduce to self-definition, fitted inputs, or self-citation load-bearing steps. The central claim remains a feasibility proposal whose practicality assumption is unexamined but not circular by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review supplies no equations, parameters, or postulated entities; ledger is therefore empty.

pith-pipeline@v0.9.0 · 5579 in / 958 out tokens · 18667 ms · 2026-05-25T10:50:40.265860+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

17 extracted references · 17 canonical work pages

  1. [1]

    A formal library for elliptic curves in the coq proof assistant

    Evmorfia-Iro Bartzia and Pierre-Yves Strub. A formal library for elliptic curves in the coq proof assistant. InITP, volume 8558 ofLecture Notes in Computer Science, pages 77–92. Springer, 2014

    work page 2014

  2. [2]

    B. Bünz, J. Bootle, D. Boneh, A. Poelstra, P. Wuille, and G. Maxwell. Bulletproofs: Short proofs for confidential transactions and more. In2018 IEEE Symposium on Security and Privacy (SP), pages 315–334, May 2018

    work page 2018

  3. [3]

    A decision procedure for restricted intensional sets

    Maximiliano Cristiá and Gianfranco Rossi. A decision procedure for restricted intensional sets. InCADE, volume 10395 ofLecture Notes in Computer Science, pages 185–201. Springer, 2017. 8

    work page 2017

  4. [4]

    Solving quantifier-free first-order con- straints over finite sets and binary relations.Journal of Automated Reasoning, Apr 2019

    Maximiliano Cristiá and Gianfranco Rossi. Solving quantifier-free first-order con- straints over finite sets and binary relations.Journal of Automated Reasoning, Apr 2019

    work page 2019

  5. [5]

    Log as a test case generator for the test template framework

    Maximiliano Cristiá, Gianfranco Rossi, and Claudia Frydman. Log as a test case generator for the test template framework. InProceedings of the 11th International Conference on Software Engineering and Formal Methods - Volume 8137, SEFM 2013, pages 229–243, Berlin, Heidelberg, 2013. Springer-Verlag

    work page 2013

  6. [6]

    Quickchick: Property-based testing for coq

    Maxime Dénès, Catalin Hritcu, Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C Pierce. Quickchick: Property-based testing for coq. InThe Coq Workshop, 2014

    work page 2014

  7. [7]

    Aggregate cash systems: A cryptographic investigation of mimblewimble

    Georg Fuchsbauer, Michele Orrù, and Yannick Seurin. Aggregate cash systems: A cryptographic investigation of mimblewimble. InEUROCRYPT (1), volume 11476 of Lecture Notes in Computer Science, pages 657–689. Springer, 2019

    work page 2019

  8. [8]

    The bitcoin backbone protocol: Analysis and applications

    Juan Garay, Aggelos Kiayias, and Nikos Leonardos. The bitcoin backbone protocol: Analysis and applications. In Elisabeth Oswald and Marc Fischlin, editors,Advances in Cryptology - EUROCRYPT 2015, pages 281–310, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg

    work page 2015

  9. [9]

    An investigation into confidential transactions.https://github

    Adam Gibson. An investigation into confidential transactions.https://github. com/AdamISZ/ConfidentialTransactionsDoc/blob/master/essayonCT.pdf. Last access: June 2019

    work page 2019

  10. [10]

    Introduction to MimbleWimble and Grin

    Tom Elvis Jedusor. Introduction to MimbleWimble and Grin. Available at:https:// github.com/mimblewimble/grin/blob/master/doc/intro.md. Last access: June 2019

    work page 2019

  11. [11]

    Mimblewimble

    Tom Elvis Jedusor. Mimblewimble. Available at:https://scalingbitcoin.org/ papers/mimblewimble.txt. Last access: June 2019

    work page 2019

  12. [12]

    Ouroboros: A provably secure proof-of-stake blockchain protocol

    Aggelos Kiayias, Alexander Russell, Bernardo David, and Roman Oliynykov. Ouroboros: A provably secure proof-of-stake blockchain protocol. InCRYPTO (1), volume 10401 ofLecture Notes in Computer Science, pages 357–388. Springer, 2017

    work page 2017

  13. [13]

    Confidential transactions write up.https://people.xiph.org/ ~greg/confidential_values.txt

    Gregory Maxwell. Confidential transactions write up.https://people.xiph.org/ ~greg/confidential_values.txt. Last access: June 2019

    work page 2019

  14. [14]

    Bitcoin: A peer-to-peer electronic cash system.Cryptography Mailing list at https://metzdowd.com, 03 2009

    Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic cash system.Cryptography Mailing list at https://metzdowd.com, 03 2009

    work page 2009

  15. [15]

    Mechanising blockchain consensus

    George Pîrlea and Ilya Sergey. Mechanising blockchain consensus. InProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pages 78–90, New York, NY, USA, 2018. ACM

    work page 2018

  16. [16]

    The Coq Development Team.The Coq Proof Assistant Reference Manual – Version V8.9.0, 2019

    work page 2019

  17. [17]

    V. Buterin. Critical update re: Dao vulnerability. Available at:https://blog. ethereum.org/2016/06/17/critical-update-re-dao-vulnerability, 2016. 9 A Excerpt of a Z Model of a Consensus Protocol The following are some snippets of a Z model of a consensus protocol based on the model developed by Pîrlea and Sergey [15]. For reasons of space we just reproduc...

    work page 2016