Total ask: 371,875 USDC
We are excited to present a comprehensive proposal to the Polkadot community aimed at developing KPVM, a formal semantics of the Polkadot Virtual Machine (PVM) using the K Framework. This project is designed to span approximately 4 months and will involve two full-time engineers, with potential follow-up work to extend PVM tooling based on the formal semantics established in this proposal.
The formalization of PVM in K offers several significant advantages that will not only enhance the security and reliability of the Polkadot ecosystem but also provide immediate value to participants of the JAM bounty program. By establishing a precise and mathematically rigorous model of PVM, we lay the foundation for diverse client development, thorough conformance testing, and the creation of advanced developer tools.
Runtime Verification (RV) is particularly well-suited to undertake this project. We have a proven track record of applying these techniques to other blockchain ecosystems, notably through our work on KEVM—a formal semantics of the Ethereum Virtual Machine (EVM). The K Framework, our flagship product, has been successfully used to analyze and verify software across various languages, including Solidity/EVM, WebAssembly (Wasm), Michelson, and more. Our existing semantics for the RISC-V RV32EM architecture will enable us to quickly and efficiently develop KPVM.
Our past work includes the development of a range of tooling based on formal semantics, such as:
We are in close contact with Parity and the developers of PVM, and after our discussions, Parity encouraged RV to apply to the Polkadot treasury to proceed with this formal specification development. We bring extensive experience in both formal verification and blockchain systems, having completed numerous blockchain audits both inside and outside of Polkadot and verified several blockchain consensus protocols.
In an increasingly digitized world, ensuring software correctness has never been more critical. This is especially true for blockchain applications, where the permissionless nature and the intertwining of financial systems and software make absolute correctness paramount. Traditional testing techniques and ad-hoc implementations have proven inadequate to secure these complex systems, as evidenced by the numerous exploits and security breaches that have occurred in recent years.
The Polkadot Virtual Machine (PVM) currently lacks a formal specification, which poses significant risks, including undetected bugs and vulnerabilities and the hindrance of new PVM client development. The K Framework offers the perfect environment to address these challenges, providing precise and executable formal definitions and a well-tested approach to developing the necessary tooling on top of this foundation.
By creating a formal semantics of PVM using the K Framework, we will establish the required level of correctness, security, and reliability for the software systems running on the Polkadot ecosystem. This foundational work is essential for the continued evolution and success of Polkadot as a leading multi-chain ecosystem, enabling a wide range of decentralized applications and services to thrive.
We welcome feedback from the community and look forward to working together to strengthen the security and reliability of Polkadot through this critical initiative.
This proposal is about creating KPVM, a formal semantics of the Polkadot Virtual Machine (PVM) using the K Framework. The project will last about 4 months and involve two full-time engineers. The main benefits of this project are:
Runtime Verification (RV) is the team working on this project. They have experience in formal verification and blockchain systems, and have worked on KEVM, a formal semantics of the Ethereum Virtual Machine (EVM).
The main problem is that PVM currently lacks a formal specification, which can lead to bugs and vulnerabilities. Creating a formal semantics of PVM using the K Framework will help make the Polkadot ecosystem more secure and reliable.
Threshold