En revidert smart-kontrakt er ikke det samme som en bevist trygg smart-kontrakt. Slither fanger kjente mønstre. Echidna fuzzer tusenvis av tilfeldige input. Men ingen av dem kan bevise at en kritisk invariant – for eksempel at summen av alle brukersaldoer aldri overstiger kontraktens faktiske beholdning – holder for absolutt alle tilstander kontrakten kan nå. Det er jobben til formell verifisering, og i 2026 har verktøyene for å gjøre dette blitt god nok til at vanlige Solidity-utviklere kan bruke dem uten en doktorgrad i logikk.

Denne tutorialen viser deg hvordan du setter opp symbolsk testing med Halmos inni et vanlig Foundry-prosjekt, hvordan du leser og tolker et motbevis (“counterexample”), og hvordan du sammenligner tilnærmingen med Certora Prover. Du får et komplett eksempelprosjekt med en bevisst innbygget feil, som verktøyene finner steg for steg. Alt kjøres lokalt på Linux, macOS eller WSL2, og du trenger ingen betalt lisens for å følge hovedløpet.

Metoden passer for alle som allerede skriver smart-kontrakter eller annen kryptorelatert infrastruktur og ønsker et sterkere sikkerhetslag enn tester og revisjoner alene kan gi. Du trenger ikke forhåndskunnskap om formell logikk – alt du trenger å forstå, bygger vi opp underveis med konkrete eksempler i samme prosjekt. Sett av to til tre timer for å følge hele løpet fra installasjon til et fullført bevis, og litt lenger hvis du også vil prøve Certora-sporet mot slutten.

Hva er formell verifisering, egentlig?

Formell verifisering handler om å bevise matematisk at en kontrakt oppfyller en spesifikasjon, i stedet for å teste et begrenset antall tilfeller og håpe at de dekker nok av tilstandsrommet. Kjernen i moderne verktøy som Halmos er symbolsk eksekvering: i stedet for å kjøre en funksjon med konkrete tall (for eksempel transfer(100)), erstatter verktøyet input med symbolske variabler og utforsker alle mulige kjørebaner samtidig som det samler opp “path conditions” – logiske betingelser som må være sanne for at nettopp den banen skal utføres.

Når alle banene er kartlagt, sendes betingelsene til en SMT-løser (Satisfiability Modulo Theories), vanligvis Z3 fra Microsoft Research. Løseren modellerer EVM-ord som bitvektorer med fast bredde, og lagring og minne som symbolske kart. Den svarer på ett enkelt spørsmål per path: finnes det en konkret verditilordning som bryter regelen din? Hvis ja, får du et konkret motbevis – nøyaktig de input-verdiene som utløser feilen. Hvis nei (og banen er fullstendig utforsket innenfor de grensene du har satt), har du et matematisk bevis for at akkurat den banen er trygg.

Det er viktig å forstå begrensningen her. Et bevis er kun så sterkt som spesifikasjonen, modellen og forutsetningene det bygger på. Beviser du en feil eller ufullstendig regel, har du ikke bevist at kontrakten er trygg – du har bevist at den feilaktige regelen holder. Hvis du utelater oppgraderbarhet, initialisering, eksterne kall, privilegerte roller eller økonomiske forutsetninger fra modellen, kan resultatet se vellykket ut uten at det sier noe om de farene du faktisk brydde deg om.

Konkret vil en SMT-løser som Z3 representere en uint256-verdi som en 256-bits bitvektor, lagringsslot som symbolske kart fra bitvektorer til bitvektorer, og hver require eller if-betingelse i koden som en logisk begrensning lagt på disse symbolske verdiene. Når Halmos når en assert, bygger den en formel som sier “finnes det verdier for alle symbolske variabler som tilfredsstiller alle path conditions samtidig som de bryter assert-betingelsen?”. Z3 svarer enten “unsat” (ingen slik tilordning finnes – banen er bevist trygg) eller “sat” med en konkret modell, som Halmos oversetter tilbake til Solidity-verdier du kan lese direkte i terminalen.

Formell verifisering vs. statisk analyse vs. fuzzing

Vi har tidligere gått gjennom hvordan du tester smart-kontrakter for sårbarheter med Slither og Echidna. De tre teknikkene utelukker ikke hverandre – de dekker forskjellige typer feil, og de beste sikkerhetsteamene i 2026 bruker alle tre i kombinasjon. Statisk analyse som Slither leser kildekoden eller bytekoden og leter etter kjente, syntaktiske mønstre uten å faktisk utføre koden. Fuzzing med Echidna kjører koden tusenvis eller millioner av ganger med genererte input, og sjekker om noen av dem bryter en påstand. Symbolsk testing med Halmos utforsker klasser av input representert som symbolske variabler, og kan derfor finne feil som krever en presis relasjon mellom flere variabler – noe en tilfeldig fuzzer sjelden snubler over av seg selv.

Ulempen med symbolsk eksekvering er “path explosion”: antallet mulige kjørebaner vokser eksponentielt med antall grener og løkker i koden. Det er derfor Halmos fungerer best på funksjoner med begrenset kompleksitet, og gjerne i kombinasjon med Foundrys invariant-tester for de delene av koden som er for store til å verifiseres symbolsk i sin helhet. Tabellen under oppsummerer forskjellene slik vi ser dem etter å ha kjørt alle tre mot samme kodebase.

EgenskapSlither (statisk)Echidna (fuzzing)Halmos (symbolsk)
Hva den beviserMønstergjenkjenning, ingen bevisIngen funn i N kjøringer, ingen garantiMatematisk bevis innenfor modellert omfang
Typisk kjøretidSekunderMinutter til timerSekunder til timer (avhenger av løkker)
Krever spesifikasjonNeiEnkle invarianterJa, eksplisitte prove_-regler
SvakhetFalske positiver, overser logikkfeilKan gå glipp av sjeldne tilstanderPath explosion ved store løkker
Integreres med FoundryDelvis (plugin)Separat verktøyFullt integrert via forge-standard-testarv

Forutsetninger og versjoner

Før du starter, sørg for at du har følgende verktøy installert. Versjonsnumrene under er de nyeste stabile versjonene tilgjengelig per 7. oktober 2026 – kontroller alltid offisielle utgivelsessider før du installerer, siden både Foundry og Certora slipper nye versjoner ofte.

  • Operativsystem: Ubuntu 22.04/24.04, macOS 14+, eller Windows 11 med WSL2
  • Foundry (forge/cast/anvil): stabil versjon v1.8.5 (nightly-bygg oppdateres daglig, siste sett 6. oktober 2026)
  • Halmos: v0.3.3 (siste tagget utgivelse på GitHub, publisert 31. juli 2025 – ingen nyere tag var publisert per research-dato)
  • Python: 3.10 eller nyere (kreves av Halmos sin pip-installasjon)
  • Solidity-kompilator: 0.8.26 eller nyere via svm (Solidity Version Manager, følger med Foundry)
  • Z3-løser: følger automatisk med Halmos sin pip-pakke, men kan også installeres separat
  • Git: hvilken som helst nyere versjon for kildekontroll
  • Minst 8 GB RAM anbefalt – symbolsk eksekvering er minnetungt på kontrakter med mange tilstandsvariabler
  • Valgfritt for sammenligning: Certora Prover 8.16.1 (publisert 15. juni 2026), krever Java og en API-nøkkel fra Certora

Du trenger grunnleggende kjennskap til Solidity og til hvordan du skriver en enkel enhetstest i Foundry. Hvis du aldri har brukt forge før, er det verdt å lese gjennom vår gjennomgang av sikker Solidity-utvikling først, siden vi ikke dekker Solidity-grunnlaget her.

Steg 1: Installer Foundry

Foundry installeres via foundryup, verktøyets egen oppdaterer. Kjør følgende i terminalen:

curl -L https://foundry.paradigm.xyz | bash
source ~/.bashrc
foundryup

# Bekreft versjon
forge --version
# forge Version: 1.8.5-stable

Hvis forge --version viser en eldre versjon, kjør foundryup på nytt. Foundry følger en rullende utgivelsesmodell med nightly-bygg hver dag, så hvis du vil ha de absolutt nyeste funksjonene (med litt mer risiko for regresjon), kan du kjøre foundryup --version nightly i stedet for stabil-sporet.

Steg 2: Installer Halmos

Halmos distribueres som en Python-pakke. Vi anbefaler et isolert virtuelt miljø for å unngå versjonskonflikter med andre Python-prosjekter på maskinen din.

python3 -m venv ~/.halmos-venv
source ~/.halmos-venv/bin/activate
pip install --upgrade pip
pip install halmos

# Bekreft installasjon
halmos --version
# halmos 0.3.3

Hvis du heller vil kjøre Halmos uten å aktivere et virtuelt miljø hver gang, kan du installere det globalt med pipx install halmos, som holder avhengighetene isolert automatisk.

Steg 3: Sett opp Foundry-prosjektet

Opprett et nytt Foundry-prosjekt og rydd bort standard-malen:

forge init halmos-tutorial
cd halmos-tutorial
rm src/Counter.sol test/Counter.t.sol script/Counter.s.sol

# Legg til Halmos sine testhjelpere som avhengighet
forge install a16z/halmos-cheatcodes --no-commit

Halmos bruker Foundry sin standard testarv (forge-std), så alle prove_-funksjoner skrives i samme filstruktur som vanlige test_-funksjoner. Dette er grunnen til at symbolsk testing med Halmos er langt mindre friksjon å komme i gang med enn separate verktøy som krever egne spesifikasjonsspråk. Kildekoden til selve verktøyet, inkludert testsuiten det er bygget med, er åpent tilgjengelig i Foundry-rammeverkets GitHub-repository, som Halmos integreres direkte mot.

Steg 4: Skriv en kontrakt med en bevisst innbygget feil

For å gjøre tutorialen konkret, bygger vi en enkel innskuddshvelv (“vault”) som lar brukere sette inn og ta ut en ERC-20-liknende intern saldo. Vi legger inn en subtil feil i withdraw-funksjonen: den sjekker ikke at brukerens saldo er stor nok før den trekker fra totalsummen, noe som kan føre til underflow-liknende tilstandskorrupsjon i visse rekkefølger av kall. Lagre denne i src/Vault.sol:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.26;

contract Vault {
    mapping(address => uint256) public balanceOf;
    uint256 public totalDeposited;

    function deposit(uint256 amount) external {
        balanceOf[msg.sender] += amount;
        totalDeposited += amount;
    }

    function withdraw(uint256 amount) external {
        // BUG: oppdaterer totalDeposited før vi har
        // bekreftet at saldoen faktisk dekker beløpet
        totalDeposited -= amount;
        balanceOf[msg.sender] -= amount;
    }

    function invariantSolvent() external view returns (bool) {
        // Skal alltid være sant: totalDeposited kan aldri
        // bli mindre enn null, og ingen bruker skal kunne
        // trekke ut mer enn de faktisk har satt inn
        return totalDeposited <= address(this).balance + 1e30;
    }
}

Siden Solidity 0.8.x har innebygd overflow/underflow-revert, vil denne konkrete feilen faktisk revertere på egen hånd i de enkleste tilfellene. Det er nettopp poenget: feilen er fanget i ett scenario, men ikke nødvendigvis i alle. Formell verifisering skal bevise at ingen sekvens av kall kan bryte invarianten – ikke bare at det ene scenarioet du tenkte på feiler trygt.

Steg 5: Skriv en vanlig Foundry invariant-test

Før vi går symbolsk, skriver vi en ordinær invariant-test slik Foundry allerede støtter den. Dette gir deg et sammenligningspunkt, og er samme teknikk som vi dekket i artikkelen om å teste mot flash loan-angrep med Foundry.

// test/Vault.invariant.t.sol
import {Test} from "forge-std/Test.sol";
import {Vault} from "../src/Vault.sol";

contract VaultInvariantTest is Test {
    Vault vault;

    function setUp() public {
        vault = new Vault();
    }

    function invariant_solvent() public {
        assertTrue(vault.invariantSolvent());
    }
}

Kjør testen med forge test --match-contract VaultInvariantTest -vvv. Du finner full dokumentasjon av Foundrys invariant-testing i den offisielle håndboken. Foundry genererer tilfeldige sekvenser av kall og sjekker invarianten etter hver av dem. Problemet: en finit testkampanje som passerer beviser ikke at invarianten holder for enhver rekkefølge av kall – den beviser bare at ingen av de sekvensene Foundry tilfeldigvis genererte, klarte å bryte den.

Steg 6: Skriv din første symbolske prove_-test med Halmos

Nå kommer kjernen i tutorialen. Opprett test/Vault.symbolic.t.sol med en prove_-funksjon i stedet for test_ eller invariant_. Halmos gjenkjenner prove_-prefikset og behandler alle parametere som symbolske variabler automatisk:

// test/Vault.symbolic.t.sol
import {Test} from "forge-std/Test.sol";
import {Vault} from "../src/Vault.sol";

contract VaultSymbolicTest is Test {
    Vault vault;

    function setUp() public {
        vault = new Vault();
    }

    /// @custom:halmos --solver-timeout-assertion 0
    function prove_withdrawNeverExceedsBalance(
        address user,
        uint256 depositAmount,
        uint256 withdrawAmount
    ) public {
        vm.assume(depositAmount > 0 && depositAmount < 1e30);
        vm.assume(withdrawAmount > 0);

        vm.prank(user);
        vault.deposit(depositAmount);

        uint256 balBefore = vault.balanceOf(user);

        vm.prank(user);
        vault.withdraw(withdrawAmount);

        // Beviset: hvis uttaket var større enn innskuddet,
        // skal kallet ha revertert, ikke lykkes
        if (withdrawAmount > balBefore) {
            assertTrue(false, "withdraw skulle ha revertert");
        }
    }
}

Legg merke til vm.assume(...)-linjene. Dette er antagelser du legger på de symbolske variablene for å begrense bevisrommet til gyldige og relevante tilfeller. Overdrevet mange assume-kall er en av fallgruvene vi kommer tilbake til nedenfor – hver antagelse kutter bort en del av tilstandsrommet, og det er lett å utelate nettopp det tilfellet feilen gjemmer seg i.

Steg 7: Kjør Halmos og tolk resultatet

Med det virtuelle miljøet aktivert, kjør Halmos fra prosjektroten:

source ~/.halmos-venv/bin/activate
halmos --function prove_withdrawNeverExceedsBalance -vv

Siden Solidity 0.8.x automatisk revert-er ved underflow, vil denne spesifikke testen faktisk passere – Halmos beviser at withdraw alltid reverterer når beløpet er for stort, for alle mulige verdier av user, depositAmount og withdrawAmount innenfor de grensene du satte. Det er nøyaktig den typen garanti du ikke kan få fra fuzzing alene: output ser slik ut når testen består:

Running 1 tests for test/Vault.symbolic.t.sol:VaultSymbolicTest
[PASS] prove_withdrawNeverExceedsBalance(address,uint256,uint256) (paths: 4, time: 1.82s, bounds: 0)
Symbolic test result: 1 passed; 0 failed

Steg 8: Lag en faktisk feil og se Halmos finne den

For å demonstrere hva et motbevis faktisk ser ut som, endrer vi kontrakten til å bruke unchecked-blokker (en vanlig gasoptimalisering som fjerner den automatiske overflow-sjekken):

function withdraw(uint256 amount) external {
    unchecked {
        totalDeposited -= amount;
        balanceOf[msg.sender] -= amount;
    }
}

Kjør samme Halmos-kommando igjen. Nå finner verktøyet et konkret motbevis, på samme måte som i a16z crypto sin egen forskningsartikkel om symbolsk testing med Halmos:

[FAIL] prove_withdrawNeverExceedsBalance(address,uint256,uint256) (paths: 4, time: 2.1s)
Counterexample:
    user    = 0x0000000000000000000000000000000000000001
    depositAmount = 1
    withdrawAmount = 2
Reason: assertion violated at line 24

Dette er den praktiske styrken i symbolsk testing: Halmos ga deg de nøyaktige input-verdiene som bryter invarianten, uten at du måtte gjette deg frem til dem eller vente på at en fuzzer tilfeldigvis skulle treffe nøyaktig den kombinasjonen. Med unchecked kan en bruker med saldo 1 trekke ut 2, og saldoen underfyller til et enormt positivt tall – en klassisk og kostbar feilklasse i DeFi-historien.

Steg 9: Håndter path explosion med grenser og oppsummeringer

Når kontrakten din har løkker – for eksempel en funksjon som itererer over en liste med mottakere – vokser antall symbolske baner raskt. Halmos lar deg sette en øvre grense for løkkeutrulling med --loop-flagget, og du kan dele opp kompliserte funksjoner i mindre interne hjelpefunksjoner som bevises separat og deretter komponeres:

halmos --function prove_batchTransfer --loop 4 --array-lengths recipients=4

Dette betyr i praksis at beviset ditt kun gjelder for lister med opptil 4 elementer. Det er ikke et fullstendig bevis for alle lengder, men det er likevel langt sterkere enn en håndfull fuzz-eksempler, og i praksis fanger det opp det store flertallet av indekserings- og akkumuleringsfeil som dukker opp uavhengig av listelengde.

Steg 10: Legg Halmos inn i CI med GitHub Actions

Et bevis som bare kjøres manuelt på utviklerens egen maskin, blir fort glemt. Legg Halmos inn som en egen jobb i CI-pipelinen slik at hver pull request kjører alle prove_-tester automatisk:

# .github/workflows/halmos.yml
name: Halmos formal verification
on: [pull_request]
jobs:
  halmos:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: foundry-rs/foundry-toolchain@v1
      - uses: actions/setup-python@v5
        with:
          python-version: "3.12"
      - run: pip install halmos
      - run: halmos --config halmos.toml

Legg gjerne til en halmos.toml-fil i prosjektroten for å definere standard timeout, løkkegrenser og hvilke kontrakter som skal inkluderes, slik at CI-oppsettet er identisk med det du kjører lokalt.

Steg 11: Sammenlign med Certora Prover

Certora Prover (siste versjon 8.16.1, utgitt 15. juni 2026) løser samme grunnproblem som Halmos, men med et eget spesifikasjonsspråk kalt CVL (Certora Verification Language) i stedet for Solidity-tester. Certora retter seg mot flere kjeder utover EVM, inkludert Solana og Stellar i tillegg til Ethereum. En enkel CVL-regel som speiler Halmos-beviset ovenfor ser slik ut:

// Vault.spec (CVL)
rule withdrawNeverExceedsBalance(address user, uint256 amount) {
    uint256 balBefore = balanceOf(user);

    env e;
    require e.msg.sender == user;
    withdraw(e, amount);

    assert amount <= balBefore,
        "withdraw skal revertere hvis beløp overstiger saldo";
}

Fordelen med Certora er et mer uttrykksfullt spesifikasjonsspråk for komplekse, tverrgående invarianter og god støtte for flere kjeder. Ulempen er at CVL er et eget språk du må lære i tillegg til Solidity, og at den fulle proveren krever en lisens fra Certora for kommersiell bruk, mens Halmos er åpen kildekode og kjører helt lokalt uten ekstern avhengighet til en sky-tjeneste. For mindre team er Halmos ofte det rimeligste stedet å starte, og du kan alltid trappe opp til Certora for de mest kritiske modulene senere.

Certora har sluppet nye prover-versjoner i jevnt tempo gjennom hele 2026, noe som er verdt å følge med på hvis du vurderer verktøyet for et produksjonsprosjekt. Tabellen under viser utgivelseshistorikken slik den var dokumentert i Certoras egne versjonsnotater per research-dato:

VersjonUtgivelsesdatoStatus per 7. oktober 2026
8.6.36. januar 2026Foreldet
8.8.09. februar 2026Foreldet
8.11.321. april 2026Foreldet
8.13.05. mai 2026Foreldet
8.16.115. juni 2026Nyeste dokumenterte versjon

Steg 12: Installer og kjør Certora Prover (valgfritt)

Hvis du vil prøve Certora Prover mot samme Vault.sol-kontrakt, installerer du klienten via pip, akkurat som med Halmos. Du trenger i tillegg Java (versjon 11 eller nyere) installert lokalt, siden selve proveren kjører som en Java-prosess under skallet:

pip install certora-cli
certoraRun --version
# Certora Prover 8.16.1

# Krever en API-nøkkel registrert hos Certora (gratis for
# åpen kildekode-prosjekter, betalt for kommersiell bruk)
export CERTORAKEY="din-api-nøkkel-her"

certoraRun src/Vault.sol --verify Vault:Vault.spec

Resultatet lastes opp til Certoras eget nettgrensesnitt, hvor du får en visuell oversikt over hvilke regler som ble bevist, hvilke som feilet, og et konkret motbevis for hver feilende regel – på samme måte som Halmos sin tekstlige counterexample-output, men med et grafisk kall-tre du kan klikke deg gjennom. For team som allerede bruker Halmos lokalt i CI, er det vanlig å reservere Certora til periodiske, dypere gjennomganger av de mest kritiske modulene rett før en større lansering, i stedet for å kjøre det på hver eneste commit.

Hurtigreferanse: de viktigste Halmos-flaggene

Når du går fra enkle eksempler til en faktisk kodebase, bruker du disse flaggene oftest. Det er verdt å lime inn tabellen under som en lapp ved siden av terminalen de første ukene:

FlaggHva det gjør
--function NAVNKjør kun en spesifikk prove_-funksjon i stedet for alle
--loop NSetter øvre grense for løkkeutrulling til N iterasjoner
--array-lengths navn=NFikser lengden på et symbolsk array til N elementer
--solver-timeout-branching MSTidsbudsjett i millisekunder per gren før løseren gir opp
--solver-timeout-assertion MSTidsbudsjett for selve assert-sjekken, uavhengig av gren-timeout
-v / -vv / -vvvØkende detaljnivå i output, nyttig for feilsøking av motbevis

Steg 13: Bygg ut spesifikasjonene dine systematisk

Den siste delen av arbeidet er ikke teknisk, men metodisk. Gå gjennom hver offentlig funksjon i kontrakten og still tre spørsmål: hvilken tilstand skal aldri være mulig etter denne funksjonen, hvilke verdier skal aldri kunne overføres til en annen adresse enn avsenderen tillater, og hvilke adgangskontroller må alltid holde uavhengig av kallerekkefølge. Omsett hvert svar til en prove_-funksjon. Vi har tidligere skrevet om hvordan man leser en ekstern revisjonsrapport riktig – samme systematikk gjelder når du skriver dine egne spesifikasjoner: start med pengeflyt og tilgangskontroll, og utvid gradvis til mer avanserte invarianter som orakeldata-konsistens og reentrancy-beskyttelse.

Komplett eksempelprosjekt: fra bug til bevist fiks

Satt sammen består det komplette prosjektet av fire filer: src/Vault.sol (kontrakten), test/Vault.invariant.t.sol (den klassiske Foundry invariant-testen), test/Vault.symbolic.t.sol (Halmos-beviset), og .github/workflows/halmos.yml (CI-jobben). Den fulle arbeidsflyten er: skriv kontrakten, skriv en symbolsk test for hver kritisk invariant, kjør halmos lokalt til alle tester passerer, fiks eventuelle motbevis Halmos finner, og lås oppsettet fast i CI slik at ingen fremtidig endring kan bryte invariantene uten at en pull request feiler automatisk. Denne arbeidsflyten er identisk uansett om kontrakten din er en enkel vault som i dette eksemplet, eller en fullverdig AMM eller lending-protokoll – kompleksiteten øker, men metoden er den samme.

Hvilke sårbarhetsklasser dekker dette i praksis?

Når du skal prioritere hvilke funksjoner som fortjener et symbolsk bevis, er det nyttig å tenke i etablerte sårbarhetsklasser i stedet for å gjette. Vi har tidligere skrevet om hvordan ERC-4337-smartkontoer sikres mot egne angrepsflater, og samme tankemønster går igjen her: hver kjent feilklasse kan oversettes direkte til en konkret prove_-mal.

SårbarhetsklasseHva du spesifiserer i Halmos
ReentrancyBevis at tilstandsendringer skjer før eksterne kall, ved å modellere et symbolsk eksternt kall som kan kalle tilbake inn
Feil adgangskontrollBevis at en funksjon kun endrer tilstand når msg.sender symbolsk settes til en autorisert adresse
Integer overflow/underflowBevis at aritmetikk utenfor unchecked-blokker alltid reverterer ved grenseoverskridelser, som i Vault-eksemplet ovenfor
OrakelmanipulasjonBevis at ingen enkelt oppdatering av en symbolsk prisverdi kan flytte en nøkkelinvariant mer enn en definert terskel
Feil avrundingBevis at avrundingsretningen aldri favoriserer brukeren på bekostning av protokollens egen balanse

Legg merke til at orakelmanipulasjon er vanskeligere å bevise fullstendig symbolsk enn de andre radene, siden den ofte involverer en ekstern pris-feed du ikke kontrollerer kildekoden til. I praksis mocker du oraklet med en symbolsk returverdi og beviser at kontraktens egen logikk håndterer ethvert mulig prisutfall trygt, selv om du ikke kan bevise at det underliggende oraklet selv er manipuleringssikkert.

Vanlige fallgruver

Formell verifisering gir en falsk følelse av trygghet når den brukes feil. Her er feilene vi ser oftest hos team som er nye i dette:

  1. Å bevise feil ting. Et bevis på at en funksjon "aldri reverterer" er verdiløst hvis det egentlig var "aldri lar saldoen bli negativ" du ønsket å garantere.
  2. Å overdrive bruken av vm.assume. Hver antagelse kutter vekk en del av tilstandsrommet. Et bevis som bare gjelder når amount < 1000 sier ingenting om hva som skjer ved større beløp.
  3. Å ignorere eksterne kall. Halmos kan modellere eksterne kontrakter symbolsk, men hvis du ikke eksplisitt inkluderer dem i modellen, antar verktøyet implisitt en forenklet oppførsel som kan skjule reentrancy-feil.
  4. Å sette løkkegrenser for lavt og tro beviset er fullstendig. Et bevis med --loop 4 sier ingenting om hva som skjer med 5 eller flere elementer i listen.
  5. Å behandle et bestått bevis som bevis på at hele kontrakten er trygg. Et bevis dekker nøyaktig den invarianten du skrev – ikke de ti andre tingene du ikke tenkte på å spesifisere.
  6. Å hoppe over oppgraderingslogikk og proxy-mønstre i modellen. Hvis kontrakten er oppgraderbar, må spesifikasjonene dine også dekke tilstanden før og etter en oppgradering, ikke bare implementasjonskontrakten isolert.

Feilsøking: de vanligste problemene

Disse problemene dukker opp igjen og igjen når team setter opp Halmos for første gang:

  1. "z3 solver not found". Z3 følger normalt med pip-installasjonen av Halmos, men på noen Linux-distribusjoner må du installere z3-solver separat med pip install z3-solver.
  2. Halmos finner ingen tester. Kontroller at funksjonsnavnet starter nøyaktig med prove_ (ikke Prove_ eller test_prove), og at kontrakten arver fra Test fra forge-std.
  3. Timeout på solver-nivå. Hvis en funksjon er for kompleks, bruk --solver-timeout-branching og --solver-timeout-assertion for å justere tidsbudsjettet per gren i stedet for å gi opp hele kjøringen.
  4. "Path explosion" – kjøringen tar evigheter. Begrens løkker med --loop, eller del opp funksjonen i mindre interne steg som bevises hver for seg og komponeres via et eget hjelpebevis.
  5. Feil Solidity-versjon kompilert. Halmos bruker samme kompilator som Foundry har satt opp i foundry.toml. Sjekk at solc-versjonen der matcher pragma-linjen i kontraktene dine.
  6. Ute av minne på store kontrakter. Symbolsk tilstand for mange lagringsvariabler vokser raskt. Kjør Halmos på én kontraktsmodul i isolasjon i stedet for hele systemet samtidig, med mocks for eksterne avhengigheter.
  7. Motbevis som ikke gir mening i praksis. Hvis Halmos finner et motbevis med en adresse som er 0x0 eller en annen spesialverdi systemet ditt uansett avviser andre steder, legg til en vm.assume som utelukker den spesialverdien eksplisitt i stedet for å ignorere funnet.
  8. CI-jobben er mye tregere enn lokal kjøring. GitHub Actions sine standard-runnere har mindre CPU og minne enn en utviklermaskin. Sett strammere timeouts i CI-konfigurasjonen, eller kjør kun et utvalg av de tyngste bevisene i CI og resten nattlig.

Avanserte tips for produksjonsbruk

Når grunnoppsettet fungerer, er det noen teknikker som skiller nybegynnerbruk fra hvordan sikkerhetsteam bruker Halmos i virkelige revisjoner. Bruk "ghost variables" – ekstra tilstand som kun eksisterer i testkontekst – til å spore akkumulert verdi over flere kall, slik at du kan bevise invarianter som strekker seg over en hel transaksjonssekvens og ikke bare ett enkelt funksjonskall. Skriv symbolske "setup"-funksjoner som plasserer kontrakten i en vilkårlig, men gyldig, startstilstand via symbolsk lagring (svm.createUint) i stedet for å alltid starte fra en tom kontrakt – dette fanger opp feil som bare oppstår etter at kontrakten har vært i bruk en stund.

Kombiner metodene i lag: la Slither kjøre på hver commit for å fange opp lavthengende frukt umiddelbart, la Echidna fuzze kontinuerlig i bakgrunnen mot de samme invariantene, og reserver Halmos for de mest kritiske pengeflyt-funksjonene der et matematisk bevis faktisk er verdt kjøretiden og vedlikeholdskostnaden. Ikke forsøk å bevise alt symbolsk – prioriter adgangskontroll, pengeflyt og orakellogikk, siden det er her kostnaden av en feil er høyest.

Til slutt: lagre motbevis Halmos finner som regresjonstester. Når du fikser en feil et bevis avdekket, konverter motbeviset til en konkret test_-funksjon med de eksakte verdiene fra counterexample-outputen. Det gir deg et raskt, konkret regresjonsvern selv i miljøer der det symbolske beviset senere blir for tregt å kjøre på hver commit.

Hvorfor dette er verdt tiden i 2026

DeFi-sektoren har ikke sluppet unna store hendelser selv i prosjekter som hadde blitt revidert på forhånd. Vi har tidligere dekket et orakelmanipulasjonsangrep med et tap på rundt 135 millioner dollar og et flash loan-angrep som kostet rundt 620 millioner dollar, samt en bredere oppsummering av at kryptosektoren samlet tapte rundt 3,63 milliarder dollar i cyberhendelser – delvis hos prosjekter som hadde gjennomgått en form for revisjon. Dette er ikke et argument mot revisjon eller fuzzing, men et argument for å legge til et tredje lag: formell verifisering fanger akkurat den typen presise, logiske feil som krever en eksakt kombinasjon av verdier for å utløses, og som derfor kan overleve både et menneskelig revisjonsøye og millioner av fuzz-iterasjoner.

Certora har offentliggjort en portefølje av sikkerhetsrapporter fra formelle verifiseringsoppdrag, inkludert et engasjement med Fragmetric Restaking (versjon 0.6.3, datert 18. juli 2025), som viser at metoden allerede brukes i produksjonsprotokoller. Vi har ikke funnet noen uavhengig bekreftet prosentandel for hvor stor andel av DeFi-protokollene som bruker formell verifisering i 2026, og oppgir derfor ikke et slikt tall – men den gradvise økningen i antall offentlige Certora- og Halmos-rapporter gjennom 2026 tyder på at metoden går fra et nisjeverktøy for de største protokollene til et mer vanlig lag i sikkerhetsstacken.

Når bør du IKKE bruke formell verifisering?

Formell verifisering er ikke riktig verktøy for alt. Hvis kontrakten din er et enkelt, lavrisiko-verktøy uten store pengebeløp involvert, er kostnaden ved å lære og vedlikeholde symbolske spesifikasjoner sannsynligvis høyere enn risikoen du reduserer. Kontrakter med svært komplekse matematiske beregninger (for eksempel avanserte AMM-kurver med flytende desimaltall simulert via fixed-point-biblioteker) kan være vanskelige å modellere symbolsk uten betydelig forenkling, og et bevis på en forenklet modell kan gi falsk trygghet. I slike tilfeller er grundig fuzzing kombinert med økonomisk simulering ofte mer realistisk enn å presse et symbolsk bevis gjennom en modell som ikke fanger den faktiske kompleksiteten.

Vurder også teamets kapasitet. Hvis ingen i teamet har tid til å lære syntaksen og tankegangen bak prove_-funksjoner og path conditions, er det bedre å investere tiden i en ekstern revisjon fra et firma med dedikerte formal-verification-spesialister, i stedet for å skrive svake eller feilaktige spesifikasjoner internt som gir en falsk grønn hake.

En nyttig tommelfingerregel er å se på total verdi låst i kontrakten (TVL) opp mot kostnaden ved å lære verktøyet. En enkel NFT-kontrakt med noen få hundre brukere har sjelden samme behov som en lending-protokoll eller en bro som flytter verdier mellom kjeder. Start i det små: velg én enkelt, kritisk funksjon, skriv ett prove_-bevis for den, og la erfaringen derfra avgjøre om det er verdt å utvide dekningen til resten av kodebasen.

Sjekkliste før kontrakten din går i produksjon

Bruk denne listen som en siste gjennomgang før en kontrakt med reell brukerverdi deployes til hovednettet. Den er ikke en fullstendig revisjonssjekkliste, men den fanger opp det formell verifisering konkret bidrar med utover det Slither og Echidna allerede dekker:

  • Hver funksjon som flytter penger har minst ett prove_-bevis knyttet til seg
  • Alle vm.assume-antagelser er dokumentert med en kommentar som forklarer hvorfor begrensningen er gyldig, ikke bare satt for å få beviset til å passere raskere
  • Løkkegrenser satt med --loop er store nok til å dekke realistiske bruksmønstre, ikke bare det minste tallet som fikk testen til å kjøre fort
  • Motbevis som tidligere ble funnet, er konvertert til permanente regresjonstester i test_-form
  • CI-pipelinen kjører Halmos på hver pull request mot hovedgrenen, ikke bare manuelt før en lansering
  • Oppgraderingslogikk og proxy-mønstre er inkludert i spesifikasjonene, ikke bare den isolerte implementasjonskontrakten
  • Du har en skriftlig oversikt over hvilke invarianter som ikke er formelt bevist, slik at teamet vet hvor den gjenværende risikoen faktisk ligger

Det siste punktet er lett å glemme, men er ofte det viktigste i praksis. Et prosjekt som er ærlig om hvor grensene for sine egne bevis ligger, har et langt bedre utgangspunkt for å prioritere videre sikkerhetsarbeid enn ett som antar at "vi kjører Halmos" automatisk betyr at alt er dekket.

Ofte stilte spørsmål

Er Halmos gratis å bruke?
Ja. Halmos er åpen kildekode under en permissiv lisens og publiseres av a16z crypto sitt forskningsteam på GitHub. Du installerer det lokalt via pip uten noen lisenskostnad.

Må jeg skrive om alle testene mine til symbolske tester?
Nei. Halmos kjører side om side med vanlige test_- og invariant_-funksjoner i samme Foundry-prosjekt. Du legger kun til nye prove_-funksjoner for de invariantene du ønsker et matematisk bevis for.

Kan Halmos erstatte en ekstern sikkerhetsrevisjon?
Nei. Et verktøy som Halmos beviser at spesifikasjonene du selv har skrevet holder. En ekstern revisjon vurderer også om du har tenkt på de riktige spesifikasjonene i utgangspunktet, og ser etter designfeil som ikke nødvendigvis er formulert som en invariant i koden din.

Hvor lang tid tar det å lære Halmos hvis jeg allerede kjenner Foundry?
De fleste utviklere som allerede skriver Foundry-tester kommer i gang med enkle prove_-funksjoner på noen timer. Å bli trygg på løkkegrenser, ghost variables og hvordan man håndterer path explosion på større kontrakter tar typisk flere uker med praktisk bruk.

Hva er forskjellen mellom Halmos og Certora Prover i praksis?
Halmos skriver du i Solidity inni det samme Foundry-prosjektet som resten av testene dine, og det kjører helt lokalt. Certora bruker et eget spesifikasjonsspråk (CVL), støtter flere kjeder utover EVM, og den fulle kommersielle proveren krever en lisens fra Certora for produksjonsbruk.

Fungerer Halmos på kontrakter skrevet i Vyper eller andre språk enn Solidity?
Halmos opererer på kompilert EVM-bytekode via Foundry sitt testrammeverk, men den praktiske brukergrensesnittet og eksemplene i offisiell dokumentasjon er bygget rundt Solidity-prosjekter. Vyper-støtte er mindre utprøvd i praksis.

Hva gjør jeg hvis Halmos aldri terminerer på en funksjon?
Sett en øvre tidsgrense med --solver-timeout-branching, reduser løkkegrensene med --loop, eller del opp funksjonen i mindre deler som bevises separat. En kjøring som aldri terminerer betyr nesten alltid at tilstandsrommet er for stort for den gitte konfigurasjonen, ikke at verktøyet er ødelagt.

Bør et nytt DeFi-prosjekt bruke formell verifisering fra dag én?
Ikke nødvendigvis fra den første commiten, men det er langt billigere å bygge inn prove_-tester parallelt med utviklingen enn å forsøke å spesifisere en allerede ferdig, kompleks kodebase i etterkant. Start med de funksjonene som flytter penger, og utvid gradvis derfra.