Het vorige artikel doorliep een end-to-end implementatie: een minimaal token-contract, off-chain statusreconstructie en een React-frontend — helemaal van `mint()` tot MetaMask. Dit artikel gaat verder waar dat eindigde: hoe test je zoiets als dit?
Ik ben (nog) geen blockchain-engineer, maar QA-patronen zijn goed overdraagbaar tussen domeinen, en lenen wat elders al werkt is hoe ik het snelst leer.
Het contract doet slechts drie dingen: `mint`, `transfer` en `burn`, maar zelfs dat is genoeg om de volledige QA-toolchain te oefenen: statische analyse, mutatietesten, gas-profiling, formele verificatie.
De code staat in `egpivo/ethereum-account-state`.
Blockchain QA-piramide: van statische analyse aan de basis tot formele verificatie aan de topVoordat we iets nieuws toevoegden, had het project al:
Alle tests slaagden. Coverage zag er goed uit. Dus waarom de moeite nemen voor meer?
Omdat "alle tests slagen" niet betekent "alle bugs zijn gevonden". 100% line coverage kan nog steeds een echte bug missen als geen enkele assertie het juiste controleert.
Slither (Trail of Bits) vangt problemen die onzichtbaar zijn voor tests: reentrancy, ongecontroleerde retourwaarden, interface-mismatches.
./scripts/run-qa.sh slither
Resultaat: 1 Medium-bevinding: `erc20-interface`: `transfer()` retourneert geen `bool`.
Dit is te verwachten. Het contract is opzettelijk geen volledige ERC20: het is een educatieve state machine. Maar de bevinding is niet academisch:
Als iemand later dit token importeert in een protocol dat ERC20 verwacht, zou de interface-mismatch stilletjes falen. Slither markeert het nu zodat de beslissing bewust is.
./scripts/run-qa.sh coverageCoverage-resultaat.
Eén niet-gedekte functie: `BalanceLib.gt()`. We komen hier later op terug.
forge coverage-output: 24 tests geslaagd, Token.sol coverage tabel./scripts/run-qa.sh gas
Baseline gaskosten voor de drie operaties:
Gas in termen van operatiesBij volgende runs vergelijkt `forge snapshot — diff` met de baseline. Een 20% gas-regressie in `transfer()` is een echte kost voor elke gebruiker — het opvangen voor de merge is goedkoop.
Dit is waar het interessant werd. Gambit (Certora) genereert mutanten: kopieën van `Token.sol` met kleine opzettelijke bugs (`+=` naar `-=`, `>=` naar `>`, voorwaarden omgekeerd). De pipeline voert de volledige testsuite uit tegen elke mutant. Als een mutant overleeft (alle tests slagen nog steeds), is dat een concrete test gap.
./scripts/run-qa.sh mutation
Resultaat: 97,0% mutatiescore — 32 gedood, 1 overleefde van 33 mutanten.
Gambit's output-log toont elke mutant en wat er veranderde. Een paar voorbeelden:
Generated mutant #7: BinaryOpMutation — Token.sol:168
totalSupply = totalSupply.add(amountBalance) → totalSupply = totalSupply.sub(amountBalance)
KILLED by test_Mint_Success
Generated mutant #19: RelationalOpMutation — Token.sol:196
if (!fromBalance.gte(amountBalance)) → if (fromBalance.gte(amountBalance))
KILLED by test_Transfer_Success
Generated mutant #28: SwapArgumentsMutation — Token.sol:81
return Balance.unwrap(a) > Balance.unwrap(b) → return Balance.unwrap(b) > Balance.unwrap(a)
SURVIVED ← geen test heeft dit gevangenGambit mutatietesten: 32 gedood, 1 overleefde, mutatiescore 97,0%
De overlevende mutant verwisselde `a > b` naar `b > a` in `BalanceLib.gt()`. Geen test heeft het gevangen omdat `gt()` dode code is. Het wordt nergens aangeroepen in `Token.sol`.
Coverage markeerde 91,67% functies maar kon de gap niet verklaren. Mutatietesten wel: `gt()` is dode code, niets roept het aan en niemand zou het merken als het fout was.
Dode of onbeschermde code in smart contracts heeft reële precedenten.
De functie was niet bedoeld om aanroepbaar te zijn, maar niemand testte die aanname. Onze `gt()` is onschadelijk in vergelijking, maar het patroon is hetzelfde: code die bestaat maar nooit wordt uitgevoerd is code waar niemand naar kijkt.
Halmos (a16z) redeneert over alle mogelijke invoer symbolisch. Waar fuzz-tests willekeurige waarden samplen en hopen edge cases te raken, bewijst Halmos eigenschappen exhaustief.
./scripts/run-qa.sh halmos
Resultaat: 9/9 symbolische tests slagen — alle eigenschappen bewezen voor alle invoer.
Geverifieerde eigenschappen:
Geverifieerde eigenschappenEen praktische opmerking: Halmos 0.3.3 ondersteunt `vm.expectRevert()` niet, dus kon ik geen revert-tests schrijven op de normale Foundry-manier. De workaround is een try/catch-patroon — als de aanroep slaagt terwijl het zou moeten reverten, faalt `assert(false)` het bewijs:
function check_mint_reverts_on_zero_address(uint256 amount) public {
vm.assume(amount > 0);
try token.mint(address(0), amount) {
assert(false); // zou hier niet moeten komen
} catch {
// verwachte revert - Halmos bewijst dat dit pad altijd wordt genomen
}
}
Niet het mooiste, maar het werkt — Halmos bewijst nog steeds de eigenschap voor alle invoer. Dit is het soort ding dat je alleen ontdekt door de tool daadwerkelijk uit te voeren.
Voor context waarom formele verificatie belangrijk is:
De kwetsbaarheid zat in de code, te beoordelen door iedereen, maar geen tool of test heeft het voor deployment gevangen. Symbolische provers zoals Halmos bestaan precies om die gap te dichten — ze samplen niet; ze doorlopen de volledige invoer ruimte.
Halmos-output: 9 tests geslaagd, 0 gefaald, symbolische test resultatenHet testbestand is `contracts/test/Token.halmos.t.sol`.
De architectuur van het eerste artikel heeft een TypeScript-domainlaag die de on-chain state machine spiegelt. Deze fase test of de twee daadwerkelijk overeenkomen.
Ik voegde fast-check property-tests toe voor de TypeScript-domainlaag, die spiegelen wat Foundry's fuzzer doet voor Solidity:
npm test - tests/unit/property.test.ts
Resultaat: 9/9 property-tests slagen na het fixen van een echte bug.
Geteste eigenschappen:
fast-check vond een echte cross-layer consistentiebug in `Token.ts` `transfer()`. Het verkleinde tegenvoorbeeld was onmiddellijk duidelijk:
Property failed after 3 tests
Shrunk 2 time(s)
Counterexample: transfer(from=0xaaa…, to=0xaaa…, amount=1n)
→ from == to (self-transfer)
→ verifyInvariant() returned false
Self-transfer (`from == to`) brak de `sum(balances) == totalSupply` invariant. `toBalance` werd gelezen voordat `fromBalance` was bijgewerkt, dus wanneer `from == to`, overschreef de verouderde waarde de aftrekking:
// Voor (buggy)
const fromBalance = this.getBalance(from);
const toBalance = this.getBalance(to); // ← verouderd wanneer from == to
this.accounts.set(from.getValue(), fromBalance.subtract(amount));
this.accounts.set(to.getValue(), toBalance.add(amount)); // ← overschrijft de aftrekking
Fix: lees `toBalance` na het schrijven van `fromBalance`, overeenkomend met Solidity's storage-semantiek:
// Na (gefixt)
const fromBalance = this.getBalance(from);
this.accounts.set(from.getValue(), fromBalance.subtract(amount));
const toBalance = this.getBalance(to); // ← leest nu bijgewerkte waarde
this.accounts.set(to.getValue(), toBalance.add(amount));
Het Solidity-contract was niet getroffen: het herleest storage na elke schrijfoperatie. Maar de TypeScript-mirror had een subtiele ordering-dependency die geen enkele bestaande unit-test dekte.
Cross-layer mismatches op grotere schaal zijn catastrofaal geweest.
Onze self-transfer bug zou niemand geld hebben gekost, maar de failure mode is structureel hetzelfde: twee lagen die zouden moeten overeenkomen, doen dat niet.
QA-tools draaien op een bestaand project is nooit gewoon "installeren en draaien". Een paar dingen gingen kapot voordat ze werkten:
Alles draait via twee scripts:
./scripts/run-qa.sh slither gas # alleen statische analyse + gas
./scripts/run-qa.sh mutation # alleen mutatietesten
./scripts/run-qa.sh all # alles
Niet elke check is snel. Slither en coverage draaien bij elke commit. Mutatietesten en Halmos zijn langzamer — beter geschikt voor wekelijkse of pre-release runs.
Vijf QA-lagen, elk vangt een andere klasse van problemen.
Laag-uitlegGambit en fast-check gaven de meest bruikbare resultaten in deze ronde.
De QA-checks zijn nu aangesloten op GitHub Actions als een zeslaags pipeline:
CI Pipeline: Build & Lint vertakt naar Test, Coverage, Gas, Slither en Audit stagesGitHub Actions pipeline: Build & Lint controleert alle downstream stages.
Stage-uitlegEthereum Account State: QA Pipeline for a Minimal Token werd oorspronkelijk gepubliceerd in Coinmonks op Medium, waar mensen het gesprek voortzetten door dit verhaal te highlighten en erop te reageren.


