Gluon Stablecoin Protocol - Research Paper and Formal Verification

[GENERAL] Name and surname of main applicant

Dr. Bruno Woltzenlogel Paleo (a.k.a. Zahnentferner) -- Djed Alliance -- The Stable Order

[GENERAL] Are you delivering this project as an individual or as an entity (whether formally incorporated or not)

Entity (Not Incorporated)

[GENERAL] Co-proposers and additional applicants

• Luca D'Angelo - He is the lead blockchain developer at zenGate Global, working on the Palmyra platform and the Winter traceability protocol. He has been involved in the Ergo blockchain community working as a smart-contract developer on various projects including Lilium, Phoenix Finance, 4EYES, Blitz TCG, ErgoNames, GuapSwap, EXLE, ErgoPad, and most recently The Stable Order within the Stability Nexus for the Gluon Gold protocol deployed on the Ergo testnet. He holds a B.Sc. in physics and computer science from McGill University.

• Mohammad Shaheer - He graduated from Carnegie Mellon University with a Bachelor’s in Computer Science and concentration in Algorithms and Complexity. While working on his senior year thesis, he developed an interest in the Blockchain technology particularly about Formal Verification of Smart Contracts and Stablecoins. His thesis focused on Formal Verification of Blockchain Oracles using the Coq Interactive Theorem Prover. Demonstrating a deep understanding, he validated essential properties concerning economic fairness and sustainability within the oracle protocol. He was successful in getting his work accepted for the TYPES 2023 conference where he and his team shared insights from their work. Beyond Blockchain Oracles, Mohammad remains engaged in refining stablecoin protocols and their Formal Verification. He exhibits a profound interest in logic and theorem provers, leveraging these tools to craft secure and reliable software systems.

[GENERAL] Please specify how many months you expect your project to last (from 2-12 months)

6

[GENERAL] Please indicate if your proposal has been auto-translated into English from another language

No

[GENERAL] Summarize your solution to the problem (200-character limit including spaces)

Gluon is a completely novel stablecoin protocol inspired by nuclear physics that allows fissioning any asset into its stable and volatile "tokeons", fusioning them back and decaying one to the other.

[GENERAL] Does your project have any dependencies on other organizations, technical or otherwise?

No

[GENERAL] If YES, please describe what the dependency is and why you believe it is essential for your project’s delivery. If NO, please write “No dependencies.”

No dependencies.

[GENERAL] Will your project’s output/s be fully open source?

Yes

[GENERAL] Please provide here more information on the open source status of your project outputs

The paper and the formal verification documents will be released under CC-BY-SA-NC license to a public repository of papers (most likely eprint).

[SOLUTION] Please describe your proposed solution

Gluon is a completely novel type of stablecoin protocol. Instead of issuing a new token (i.e. the stablecoin), Gluon "breaks" an existing token into its stable and volatile components. To do so, it takes inspiration from nuclear physics:

Similarly to how nuclear fission breaks an atomic nucleus made of neutrons and protons, Gluon's fission operation breaks a token into stable and volatile "tokeons".

Thus, Gluon is the first stablecoin protocol where the stablecoin is not a new asset, but is rather a "sub-asset" or an "asset particle".

Similarly to nuclear fusion's merging of nuclear particles into bigger nuclei, Gluon's fusion operation merges tokeons back into the original token.

Gluon's two other fundamental operations take inspiration from beta decays, which transform protons into neutrons and vice versa, to allow users to swap stable and volatile tokeons for each other.

Gluon can also be seen as a dual of a liquidity pool: whereas in a liquidity pool that user deposits two assets and gets an LP token; in Gluon the user deposits a token and gets two tokeons. Like in liquidity pools, Gluon uses mechanisms to disincentivize large swaps (a.k.a. beta decays).

https://www.youtube.com/watch?v=tnvm1we6xts

A Gluon-based Gold-pegged stablecoin is already live in Ergo's testnet (see https://gluon.gold). Once it is launched on Ergo's mainnet, it is only a matter of time for it to become available on Cardano as well via the Rosen Bridge.

Gluon is being researched and developed by The Stable Order, the same group that did the original research and development of the Djed stablecoin protocol. As in the case of Djed, we would like Gluon to have a high quality research paper, with stability theorems, mathematical proofs of these theorems and formal verification of these proofs. The goal of this Catalyst project is to produce this paper.

It is important to note that Gluon and Djed do not compete. They serve different niches within the Stablecoin design space. Djed has a narrower peg range and stricter reserve ratio requirements. Gluon is expected to be more resistant to oracle issues, but at the cost of a wider peg range in times of high volatility.

Gluon is named after the sub-atomic particle responsible for stability of all matter in the universe.

[IMPACT] Please define the positive impact your project will have on the wider Cardano community

Cardano will benefit from Gluon as a whole and from this project in particular in multiple ways:

1 - Through the Rosen Bridge, Cardano will soon have a Gold-pegged Gluon-based stablecoin. (Here is a tutorial on how to use the Rosen bridge to bring Ergo stablecoins to Cardano: https://medium.com/djed-alliance/buy-and-hodl-sigusd-rsv-on-cardano-c10c3ce32b95)

2 - This paper will pave the way for native implementations of Gluon on Cardano.

3 - Funding of this paper will cement Cardano's reputation as a blockchain that nurtures research and innovative stablecoins.

4 - This paper will contribute to increasing public confidence about Gluon-based stablecoins on Cardano.

[CAPABILITY & FEASIBILITY] What is your capability to deliver your project with high levels of trust and accountability? How do you intend to validate if your approach is feasible?

Dr. Bruno Woltzenlogel Paleo (Zahnentferner) has been the Director of Engineering for IOG and has been responsible for designing Cardano's native multi-assets approach, allowing anyone to launch tokens on Cardano. Bruno is also a member of the original team who did the R&D for the Djed Stablecoin protocol and he is one of the 4 authors of the Djed paper. He has already published more than 100 papers, and many of those are highly cited in the fields of logic, automated reasoning and formal methods (cf. Google Scholar profile: https://scholar.google.com/citations?hl=en&user=m8dFEawAAAAJ&pagesize=100&view_op=list_works). He is a founder of the Djed Alliance, The Stable Order and the Stability Nexus and the founder of AOSSIE, a not-for-profit charity registered in Australia dedicated to open-source software innovation and education. Throughout his career, his research and development projects have received millions of dollars from sources such as various national research agencies, Catalyst and Google.

Luca D'Angelo's background in Physics is going to be helpful with the intuitions behind a nuclear physics inspired protocol. Having been also a developer of various blockchain protocols and projects (Palmyra, Winter, Lilium, Phoenix Finance, 4EYES, Blitz TCG, ErgoNames, GuapSwap, EXLE, ErgoPad, hodlCoin and Gluon Gold) will allow him to ensure that the paper is accessible not only to researchers but also to devs.

Mohammad Shaheer is a rare formal methods specialist whose thesis focused on Formal Verification of Blockchain Oracles using the Coq Interactive Theorem Prover and who has already published a paper about a formalization of an oracle protocol in the Coq theorem prover. These skills are exactly what we need for the formal methods part of our Catalyst project.

To know more about our organization as a whole, check the following links:

• https://docs.stability.nexus/
• https://medium.com/DjedAlliance
• https://news.stability.nexus/
• https://x.com/DjedAlliance
• https://x.com/StabilityNexus
• https://linkedin.com/company/stability-nexus
• https://t.me/StabilityNexus
• https://discord.gg/YzDKeEfWtS
• https://github.com/StabilityNexus
• https://djed.one/
• https://github.com/DjedAlliance
• https://eprint.iacr.org/2021/1069

[PROJECT MILESTONES] What are the key milestones you need to achieve in order to complete your project successfully?

Milestone Output: Section describing the protocol mathematically.

Acceptance Criteria: each protocol operation should be clearly mathematically defined. The definitions should specify which assets are provided by the user and which assets are given to the user.

Evidence of Milestone Completion: we will share a draft of the paper with the reviewers, containing the section with the equations of the protocol.

Estimated Length: 1 month

Milestone Output: Section containing the stability theorems and their mathematical proofs.

Acceptance Criteria: The proofs should be complete enough to be formally verifiable.

Evidence of Milestone Completion: we will share a draft of the paper with the reviewers, containing the section with the stability theorems and their mathematical proofs.

Estimated length: 2 months.

Milestone Output: formal verification of the stability proofs.

Acceptance Criteria: The formal verification should be done in a tool such as Coq, Isabelle or Lustre.

Evidence of Milestone Completion: we will share the source code of the formal verification with the reviewers.

Estimated Length: 2 months.

Milestone Output: sections with introduction, related work and conclusion. Final polishing of the paper and publication in a public academic paper repository such as eprint or arxiv.

Acceptance Criteria: the paper should appear in the chosen public academic paper repository.

Evidence of Milestone Completion: we will provide a link to the published paper.

Estimated length: 1 month.

[RESOURCES] Who is in the project team and what are their roles?

• Dr. Bruno Woltzenlogel Paleo (Zahnentferner) has been the Director of Engineering for IOG and has been responsible for designing Cardano's native multi-assets approach, allowing anyone to launch tokens on Cardano. Bruno is also a member of the original team who did the R&D for the Djed Stablecoin protocol and he is one of the 4 authors of the Djed paper. He has already published more than 100 papers, and many of those are highly cited in the fields of logic, automated reasoning and formal methods (cf. Google Scholar profile: https://scholar.google.com/citations?hl=en&user=m8dFEawAAAAJ&pagesize=100&view_op=list_works). He is a founder of the Djed Alliance, The Stable Order and the Stability Nexus and the founder of AOSSIE, a not-for-profit charity registered in Australia dedicated to open-source software innovation and education. Throughout his career, his research and development projects have received millions of dollars from sources such as various national research agencies, Catalyst and Google.
• Roles: protocol engineer, paper author, project manager.

• Luca D'Angelo - He is the lead blockchain developer at zenGate Global, working on the Palmyra platform and the Winter traceability protocol. He has been involved in the Ergo blockchain community working as a smart-contract developer on various projects including Lilium, Phoenix Finance, 4EYES, Blitz TCG, ErgoNames, GuapSwap, EXLE, ErgoPad, and most recently The Stable Order within the Stability Nexus for the Gluon Gold protocol deployed on the Ergo testnet. He holds a B.Sc. in physics and computer science from McGill University.
• Roles: paper author, responsible for the mathematical proofs in the paper.

• Mohammad Shaheer - He graduated from Carnegie Mellon University with a Bachelor’s in Computer Science and concentration in Algorithms and Complexity. While working on his senior year thesis, he developed an interest in the Blockchain technology particularly about Formal Verification of Smart Contracts and Stablecoins. His thesis focused on Formal Verification of Blockchain Oracles using the Coq Interactive Theorem Prover. Demonstrating a deep understanding, he validated essential properties concerning economic fairness and sustainability within the oracle protocol. He was successful in getting his work accepted for the TYPES 2023 conference where he and his team shared insights from their work. Beyond Blockchain Oracles, Mohammad remains engaged in refining stablecoin protocols and their Formal Verification. He exhibits a profound interest in logic and theorem provers, leveraging these tools to craft secure and reliable software systems.
• Roles: formal methods specialist, responsible for formal verification of the proofs.

[BUDGET & COSTS] Please provide a cost breakdown of the proposed work and resources

Assumption: 1 ADA = 0.40 USD

According to Indeed (https://www.indeed.com/career/researcher/salaries), the average monthly salary of a researcher is approximately 17000 ADA.

This project's team consists of 3 researchers and we estimate that we may need 6 months to complete it. 3 x 6 x 17000 ADA = 306000 ADA.

We are requesting 100000 ADA, which is the maximum amount allowed in the "Concept" category.

[VALUE FOR MONEY] How does the cost of the project represent value for money for the Cardano ecosystem?

As explained in the budget section, we are requesting funds to cover only about one third of the cost that we estimate to have with this project. The other two thirds we will cover on our own. Therefore, this is good value for money, because Cardano will have funded a novel stablecoin paper for one third of the price that it costs. Funding of this paper will further cement Cardano's reputation as a blockchain that nurtures research and innovative stablecoins.