#011: Formal Verification of Multi-Sig & Escrow Logic (Kani / SMT)

[bakarezainab]

#11: Formal Verification of Multi-Sig & Escrow Logic (Kani / SMT)

Overview

Add Kani model checking harnesses and formal verification specs for token initialization and balance invariants.

Objectives

• Build formal proof harnesses verifying no unlocked funds can be withdrawn by non-owners.
• Verify mathematically that contract balance equals sum of vault deposits minus payouts.
• Detect potential integer overflow/underflow or state machine flaws.

Acceptance Criteria

• Kani verification harness added under src/kani_proofs.rs.
• Proofs passing without counterexamples.
• CI integration for formal verification checks.

[ebubeb683-ship-it]

I have gone through the issue details and already have an approach in mind. I would appreciate being assigned to this task.

[Okorie2000-code]

Hi maintainer, would love to work on this issue, i have already reviewed the description and will submit a clean PR. kindly assign.

[MoscowDev]

I’d love to take this issue on. I’ve worked on production-ready applications and collaborated extensively through GitHub workflows. I’ll dig into the current setup, implement a solid and reliable fix, and deliver a well-tested PR. My focus is on clean, maintainable code and fast, dependable delivery.

[Glam26]

Hi! I'd like to work on this.

My approach will be to first understand the existing implementation and how it fits into the surrounding codebase. Then I'll implement the requested changes, add or update tests where appropriate, and verify everything by running the project's linting, test suite, and build before opening a PR.

I'll keep the scope focused on the issue and document any important implementation decisions in the PR. Looking forward to contributing!

[Skinny001]

Hi, I'd like to work on this issue.

I'll add Kani verification harnesses to formally verify the multi-signature and escrow logic, including ownership, balance invariants, and overflow safety. I'll integrate the proofs into CI, ensure they pass without counterexamples, and validate that the implementation meets all acceptance criteria.

Could this issue be assigned to me? Thanks.

[grantfox-oss]

🦊 GrantFox — @Skinny001 has been assigned to this issue as part of the Official Campaign | FWC26 campaign!

Next steps:

1. Open a Pull Request referencing this issue (e.g., Closes #11)
2. Your PR will be reviewed by the LatterFixxx maintainers

Good luck! Track your progress on GrantFox.