Create Formal_Verification_of_Core_Polkadot_Runtime_Functionality.md

[SurfingBowser]

Project Abstract

This application is a follow-up grant to "Preparing Polkadot's pallet_balances for Formal Verification using the Inference Framework" (completed & merged September 9th 2025).

We plan to apply our Rocq-based framework Inference to create formally verified specifications.

Grant level

• Level 1: Up to $10,000, 2 approvals
• Level 2: Up to $30,000, 3 approvals
• Level 3: Unlimited, 5 approvals (for >$100k: Web3 Foundation Council approval)

Application Checklist

• The application template has been copied and aptly renamed (project_name.md).
• I have read the application guidelines.
• Payment details have been provided (Polkadot AssetHub (USDC & DOT) address in the application and bank details via email, if applicable).
• I understand that an agreed upon percentage of each milestone will be paid in vested DOT, to the Polkadot address listed in the application.
• I am aware that, in order to receive a grant, I (and the entity I represent) have to successfully complete a KYC/KYB check.
• The software delivered for this grant will be released under an open-source license specified in the application.
• The initial PR contains only one commit (squash and force-push if needed).
• The grant will only be announced once the first milestone has been accepted (see the announcement guidelines).
• I prefer the discussion of this application to take place in a private Element/Matrix channel. My username is: @_______:matrix.org (change the homeserver if you use a different one)

[SurfingBowser]

I have read and hereby sign the Contributor License Agreement.

[keeganquigley]

Hi @SurfingBowser thanks for the application. A few initial questions:

• I'm not seeing anything about publications in the application. Would you aim to publish your research somewhere after the grant is completed?
• Additionally, do you plan to perform differential fuzzing between the verified ink! contract and the actual pallet to prove they rely on the same logic?

Thanks for any further insights you can provide.

[SurfingBowser]

Hello @keeganquigley thanks for the questions and follow up. Here are some clarifications on the first point.

• I'm not seeing anything about publications in the application. Would you aim to publish your research somewhere after the grant is completed?

We have a final research article included under milestone 3 deliverable 0e.
It will cover our research findings regarding the proven theorems, the reusable tactics developed and a summary of the project. The article will also include details from deliverables 1 and 2.
We will have the article available both on github and our website.

For github it would be a similar format as the final research article of the previous grant Preparing Polkadot pallet Balances for Formal Verification.

Milestone 3 — Verified Proof by Custom Tactics

Number	Deliverable	Specification
0a.	Copyright and Licenses	MIT
0b.	Documentation/Tutorial	We will provide inline documentation for the proof scripts and a tutorial explaining how to execute the proofs and utilize the generalized tactics.
0c.	Reproducibility	We will provide step-by-step guides for the grants team to know what we have done. We will provide a detailed explanation of the formal proof strategies, describing how the logic was verified against the specifications and how reusable tactics were abstracted from the specific proofs.
0d.	Infrastructure	We will provide a Dockerfile that can be used to test all the functionality delivered with this milestone. It will contain the Rocq 8.20 environment with all required dependencies, modified WasmCert-Coq mechanization and our reasoning theory.
0e.	Final Research Article	We will publish a detailed research article to the Github repository and our website that explains our research findings regarding the proven theorems and the reusable tactics developed. It will also include details from deliverables 1 and 2.
1.	Proven theorems	Each statement, formalized on the previous milestone, will receive proof reaching qed without admits. Every non-trivial logic transition will be comprehensively explained in comments.
2.	Generalized tactics	We will distill methods used through such proofs into a collection of tactics, general enough to facilitate future reuse. Resulting frame_tactics.v will aggregate only proof helpers, detached from particularities of subject contract.

Documentation and tutorials are also included in milestones 1 &2, should we add an article deliverable to these milestones as well?
Please let us know if there is anything else to consider or clarify.

• Additionally, do you plan to perform differential fuzzing between the verified ink! contract and the actual pallet to prove they rely on the same logic?

It is something we have considered previously but @Keyholder will share some detailed thoughts on it.

[Keyholder]

Additionally, do you plan to perform differential fuzzing between the verified ink! contract and the actual pallet to prove they rely on the same logic?

This is something we have considered doing, but differential fuzzing of a contract compared to a pallet can be a bit tedious from the testing stand set up perspective - due to significant odds between execution environment of pallet and contract it can turn into an engineering endeavor of an unknown scale. The current scope of the project was supposed to become mostly a mathematician's job, so sudden programming roadblocks, that could arise from such comparative fuzzing, may have significant impact on delivery timeframes.

As infrastructure verification does not depend on business logic, it may be more reasonable for now to rely on existing conformance tests and allocate some time for differential fuzzing in the later stages, when accounting properties will be directly addressed. Into the current scope this may be added as a stretch goal - if the time will be limited, then we complete this after.

[keeganquigley]

Thanks for your answer @SurfingBowser I will mark the application as ready for review and ping the committee for comment.