BC8: Testing and securing smart contracts
Invariants, fuzzing and analysis tools
🎯You'll be able to
Write invariant tests, and explain what fuzzing, static analysis and formal verification add.
🏠The everyday picture
A shopkeeper who counts the till at the end of every day, not only after big sales: whatever happened, the cash should match the receipts.
📘What it really is
-
Invariants: facts that should hold after any sequence of actions, such as "the fund's ether equals the sum of members' balances".
-
Invariant tests: run many random actions and check the invariant after each. The kit's test 09 runs 60 seeded random deposits and withdrawals.
-
Fuzzing: tools such as Foundry and Echidna generate many inputs and sequences automatically, searching for a broken invariant.
- Static analysis: tools such as Slither read the code for known risky patterns without running it.
- Formal verification: proves properties mathematically for all inputs; powerful and costly, used for high-value contracts.
- Coverage: which lines and branches tests ran. High coverage helps, but doesn't prove safety.
📝A worked example
Input: a learner's SakhiFund passes tests 1 to 8 but fails test 09.
Steps:
- The failure message says the ether and the records differ after action 23.
- Action 23 was a withdrawal of a member's whole balance.
- The code reduced
balanceOfbut forgottotalDepositsin one branch. Fixing it makes all 60 actions pass.
Expected output: a bug that example tests missed, found by an invariant.
🌍Where it's used
- DeFi protocols run invariant fuzzing in CI.
- Audits use static analysis as a first pass.
- High-value contracts pay for formal verification.
📝Case scenario
A token passed its unit tests, but a fuzzing run found that transferring to yourself doubled your balance in one edge case. The team fixed it before launch. Without the invariant "total supply equals the sum of balances", the bug would have shipped.
🖱️Try it
Write two invariants for SakhiVault. Success: for example "an executed transaction can't run again" and "the threshold is between 1 and the number of owners".
⚠️Common mistakes
- Only example tests. Sign: edge cases missed. Fix: invariant tests.
- Trusting coverage numbers. Sign: "100% coverage, so it's safe". Fix: invariants and review.
- Claiming tool results you didn't run. Sign: "audited by Slither" with no output. Fix: say what was run, or "not verified".
🛠️For your project
Project 1's test 09 is an invariant test. Your security review's "Not verified" section should say if you didn't use fuzzing or static analysis.
✅Quick check
What is an invariant?
Show the answer
A fact that should hold after any sequence of actions.
Why doesn't 100% coverage prove a contract is safe?
Show the answer
Running every line once doesn't test every input or sequence.