Verified State-Lifecycle & Protocol Correctness Toolkit for Filecoin Rust Infrastructure

# Filecoin Protocol Correctness and Verification Toolkit

## Summary

I am proposing an initial research and engineering project to identify a correctness-critical component in Filecoin's Rust infrastructure and determine whether stronger invariant testing or formal verification would be useful.

I do not want to assume that Filecoin needs a new state lifecycle or expiry mechanism.

The first step would instead be to study an existing Filecoin component, its implementation, specifications, tests and known failure modes, then define the properties that should always hold.

If that analysis identifies a useful target, I would build an open-source verification harness around it.

## Background

I am a Rust systems and protocol engineer interested in distributed systems and software correctness.

My public work includes:

- Rust distributed and state-machine systems
- consensus and protocol implementation
- property-based and adversarial testing
- Kani bounded verification
- Z3 invariant checking
- TLA+ specifications
- Rocq/Coq formalisation

GitHub:

https://github.com/ss1738

One of my research projects, EvaporChain, includes experimental state lifecycle mechanisms and machine-checked Rocq/Coq properties.

I am not proposing to transplant EvaporChain's mechanism into Filecoin. I want to use the verification experience from that work on a Filecoin-specific problem.

## Milestone 1: Identify and Model a Filecoin Correctness Target

I would begin by studying Filecoin's existing Rust implementation, specifications, tests and open engineering discussions.

The goal is to identify one component where correctness depends on properties such as:

- deterministic state transitions
- persistence and recovery
- protocol validation
- lifecycle transitions
- serialization boundaries
- upgrade behaviour
- other state-machine invariants

Deliverables:

1. Description of the selected component and why it is worth verifying
2. State-transition model
3. Explicit safety/correctness invariants
4. Review of existing test coverage
5. Adversarial and failure scenarios
6. Verification feasibility report
7. Proposed implementation scope for the next milestone

Requested funding for Milestone 1:

**$5,000**

I am comfortable treating this as a standalone milestone.

If the analysis does not identify a sufficiently valuable verification target, I would recommend stopping rather than building unnecessary tooling.

## Milestone 2: Rust Verification Harness

If Milestone 1 identifies a useful target, I would build an open-source correctness harness using whichever techniques fit the component best.

These could include:

- property-based testing
- state-machine testing
- fuzzing
- Kani bounded verification
- invariant checking
- deterministic adversarial scenarios

Expected outputs:

- reusable Rust verification code
- Filecoin-specific test models
- documented invariants
- reproducible test cases
- counterexample/failure reporting
- CI integration if useful

Estimated budget:

**$10,000**

## Milestone 3: Formal Specification

For a small number of high-value properties identified during the previous work, I would investigate machine-checked formalisation using an appropriate tool such as TLA+, Rocq/Coq or SMT-based modelling.

The intention is not to formally verify Filecoin as a whole.

The goal is to determine whether formal methods can provide useful additional assurance for a small correctness-critical component.

Estimated budget:

**$10,000**

## Milestone 4: Integration and Documentation

The final milestone would focus on making the work useful to Filecoin maintainers and future contributors.

Potential deliverables:

- upstream-ready code
- documentation
- examples
- CI integration
- final technical report
- recommendations for further verification work

Estimated budget:

**$5,000 to $10,000**

## Total Potential Scope

The complete project would be approximately:

**$30,000 to $35,000**

However, I am proposing that the project begin with the **$5,000 first milestone** rather than committing to the entire scope upfront.

Later milestones should only proceed if the initial analysis demonstrates that the work would provide meaningful value to Filecoin.

## Open Source

Grant-funded code, specifications, tests and research artefacts produced through this project would be released publicly under an appropriate open-source license.

## Applicant

Satyawan Singh

GitHub:

https://github.com/ss1738

Technical areas:

Rust systems engineering, distributed systems, protocol and state-machine design, property testing, Kani, Z3, TLA+, Rocq/Coq and software verification.

I would be happy to refine the target component and technical approach based on feedback from Filecoin maintainers before beginning the work.

No specific Filecoin component, file, test, or entry point is named. Start by reviewing an existing Rust component alongside its specifications, tests, and open engineering discussions, then select a correctness target. Done means documenting the component, state-transition model, invariants, test coverage, failure scenarios, verification feasibility, and proposed follow-up scope.

Written by the indexing model from the issue text.