Grant Application
Project: RocketProof V2
Note: I am helping Ramana resubmit his Grant Application which was rejected in the previous round.
We changed the submission to an exploratory research article
What is the work being proposed?
Publish a research document on:
- What are the steps to build a formal model of the Rocket Pool protocol (the smart contracts) and its execution environment (Ethereum) in higher-order logic.
- Which components are suitable for formal verification, and what kinds of properties we can hope to verify in this style.
- Estimate the feasibility and/or resource requirements for different levels of verification.
Is there any related work this builds off of?
No, although we will use existing generic tooling and libraries e.g. https://hol-theorem-prover.org 2.
Will the results of this project be entirely open source (MIT, GPL, Apache, CC BY license or similar)? If not, which parts will not be, why, and under what license will they be published?
Pure unadulterated free software. 100% GPL.
Benefits - enter N/A where appropriate
How does this benefit Rocket Pool?
A formal model verification would bring:
- Machine-checked confidence in the safety and security of the protocol.
- A unique marketing opportunity: that the protocol has been formally verified to the proposed degree of thoroughness.
- In case any bug bounties are found to be claimable during the course of the verification, these will be claimed and mitigated, which further enhances the quality and security of the protocol. 10% of all bug bounties claimed will be donated back to the GMC budget.
What other non-RPL protocols, DAOs, projects, or individuals, would stand to benefit from this grant?
The Ethereum (both execution and consensus layer) protocol model will be reusable for other verification projects. And the methodology for smart contract protocol verification may also be reusable.
Will the resulting project be open source?
How could it possibly not be?
Team
Who is doing the work?
Ramana, Lutro
What is the background of the person(s) doing the work? What experience do they have with such projects in the past?
Ramana:
- Rocket Pool node operator, and holder of rETH and RPL
- Has an award-winning PhD in formal verification, and is a primary author of a large project in this area (cakeml.org), amongst other theorem-proving projects.
What is the breakdown of the proposed work, in terms of milestones and/or deadlines?
A research document describing the steps to build a formal model of Rocket Pool. It should take around 1 or 2 weeks depending on Ramana’s schedule.
How is the work being tested? Is testing included in the schedule?
N/A
How will the work be maintained after delivery?
N/A
Payment and Verification
We propose a budget 2000$ (around 55 RPL at today’s prices) for the feasibility paper.
What is the acceptance criteria?
Probably the best approach would be to have a meeting with the GMC and/or the RocketPool’s teams to go over the expectations for the article.
What is the proposed payment schedule for the grant? How much RPL and over what period of time is the applicant requesting?
Open to whatever the GMC suggests on this point.
How will the GMC verify that the work’s deliveries match the proposed cadence?
All development will be in a public git repository, and the team will make themselves available for Q&A as desired (within reason).
What alternatives or options have been considered in order to save costs for the proposed project?
N/A
Conflict of Interest
Does the person or persons proposing the grant have any conflicts of interest to disclose? (Please disclose here if you are a member of the GMC or if any member of the GMC would benefit directly financially from the grant).
No
Will the recipient of the grant, or any protocol or project in which the recipient has a vested interest (other than Rocket Pool), benefit financially if the grant is successful?
No