This report captures the protocol invariants that are already enforced in code and the additional proof obligations that should be preserved during future changes.
Critical paths covered by the current contract implementation:
- user lifecycle and balances
- flexi, lock, goal, and group plan transitions
- staking and rewards accounting
- governance and timelock execution
- treasury allocation and withdrawals
- emergency pause and strategy disable flows
| Invariant | Intent | Enforced In |
|---|---|---|
| Non-negative amounts | No balance or fee operation should create a negative value | src/invariants.rs, src/lib.rs |
| Fee bounds | Basis points must remain within 0-10,000 | src/invariants.rs::assert_valid_fee |
| Pause safety | Mutable operations must stop when paused | src/lib.rs, src/config.rs |
| Reentrancy safety | External interactions must not re-enter active state transitions | src/security.rs, src/lib.rs |
| Authorized ownership | Only the owning user or admin may mutate a plan or config | src/lib.rs, module-specific guards |
| Lock maturity | Locked savings must not withdraw before maturity | src/lock.rs |
| Signature freshness | Off-chain authorizations must expire | src/lib.rs::verify_signature |
| Governance control | Admin/governance transitions must preserve voting and timelock rules | src/governance.rs, src/timelock.rs |
The following properties should be kept stable and re-checked whenever money-moving logic changes:
- Deposits and withdrawals preserve the total balance accounting for fees.
- A plan marked withdrawn or completed cannot be withdrawn twice.
- Emergency withdrawal disables a plan before any repeated drain can occur.
- Treasury allocation percentages sum to 10,000 basis points.
- Governance actions obey proposal thresholds, quorum, and timelock delays.
The repository already contains direct runtime checks and targeted tests that support the invariants above:
- arithmetic guard tests in
src/lib.rs - invariant helpers in
src/invariants.rs - pause, auth, and admin-path checks in the contract modules
- strategy and governance test suites under
src/
Formal verification is modeled as a layered process rather than a single external tool:
- Encode the invariant in a small helper or guard.
- Add a targeted regression test for the invariant.
- Record the proof obligation in this report.
- Generate the docs bundle so the invariant remains visible to reviewers.
- Does the change preserve balance conservation?
- Does it introduce a new unguarded mutation path?
- Can a paused or disabled contract still mutate state?
- Can an authorization or expiry check be bypassed?
- Does the change require a new regression test or invariant helper?
The contract codebase now has a documented invariant set and a repeatable documentation/verification workflow. Future proof automation can be added without changing the published contract interface.