Program Verification Tooling

Context

Solana users and developers should have better insights into the security posture of programs they’re using or invoking. There should exist verification tooling, program scoring and APIs that let wallets, explorers and developers fetch security details about programs they’re interacting with. Additionally, auditors and program developers should be able to post attestations about the incremental audits of programs for ingestion into the tooling requested above.

Please see the following RFP that outlines a request to create program verification tooling. The Solana Foundation lays out a list of proposed solutions, but the technology used to verify programs is at the behest of the applicant.

Logistics

Take note of the application deadline (2/29/2024). The maximum grant amount is not included within the request as different security applications will have varying cost factors. The resulting finalist(s) will work with the Solana Foundation to receive an appropriate grant issued in USD-equivalent locked SOL with approachable, but rigorous milestones.

Ground Rules

This thread can be used for comments, questions, praise, and / or criticism, and is intended to be an open forum for any prospective responders. This thread is also an experiment in increasing the transparency through which RFPs are fielded by the Solana ecosystem too, so please be mindful that we’re all here to learn and grow.

Responses to this RFP are not required to be public (but recommended), but if it is helpful to share notes or combine forces, then please use this thread for such purposes


Link: Airtable - Solana Foundation Public RFP Database

1 Like

Hello, Solana community,

I’m excited to see that Solana Foundations is interested in formal method application development in this RFP. Before submitting my proposal, I seek clarity on whether it aligns with the Foundations’ expectations for this RFP.

I represent Inferara, a research group I lead that is focused on automated reasoning. We’re exploring the feasibility of formalizing specifications for blockchain systems within a proof system (e.g., Coq). We aim to create a mathematically grounded framework to aid developers in writing formal specifications and proving the properties of their code.

Our Team’s Strengths:

  • Extensive software engineering experience, including blockchain security and formal language analysis.
  • Academic expertise in mathematics, game theory, and distributed systems.

Project Overview:

  • Our research necessitates thorough preliminary studies, adopting an academic approach. For insight into our methodology, consider our article on Program Verification: background and notation.
  • The project is phased, starting with theoretical research milestones we are currently progressing in.

Inquiry to Solana Foundations:
Would the Foundations be interested in detailed, academically styled papers as deliverables? Additionally, could code examples in Coq and Rust, illustrating the discussed concepts, be valuable?

Our ultimate goal is to evolve this framework into a practical implementation. This would facilitate formal specifications and proofs for code within both Solana’s core and on-chain DApps.

I am looking forward to hearing feedback and hoping our proposal can contribute to the Solana ecosystem.

Hi @0xGeorgii apologies for the late reply here.

This would better fit under our research initiative, as these security RFPs are focused on production use cases. Please reach out to me at Telegram: Contact @pkxro

1 Like