Skip to content

Add Kani harness for vault.transfer correctness under adversarial input #490

Description

@greatest0fallt1me

Description

This is a smart-contract issue for the GrantFox campaign. Add a Kani proof harness asserting that transfer preserves total supply and respects authorization.

Requirements and Context

  • Kani harness file
  • CI workflow runs Kani on PRs
  • Proof passes
  • Doc explains harness
  • Must be secure, tested, and documented
  • Should be efficient and easy to review

Suggested Execution

  1. Fork the repo and create a branch
    git checkout -b task/kani-transfer
  2. Implement changes
    • contracts/vault/proofs/transfer.rs (new)
    • .github/workflows/kani.yml (new)
    • docs/formal-verification.md (new)
  3. Test and commit
    • Run the repo's standard test suite and lint
    • Cover edge cases; include output in the PR

Example commit message

test: Kani proof harness for vault.transfer

Acceptance Criteria

  • Harness compiles
  • CI runs
  • Proof passes
  • Doc explains

Guidelines

  • Minimum 95% test coverage with cargo test
  • require_auth on every state-changing entrypoint
  • Overflow-safe math; no unwrap() in production paths
  • Clear NatSpec-style /// rustdoc
  • Timeframe: 96 hours

Metadata

Metadata

Assignees

Labels

GRANTFOX OSSGrantFox open-source campaign taskOFFICIAL CAMPAIGNOfficial GrantFox campaign issueStellar WaveIssues in the Stellar wave programauditSecurity audit/reviewsmart-contractSoroban smart-contract worktestingTests and coverage

Type

No type
No fields configured for issues without a type.

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions