Patrick Azzopardi (Dowsers): "Wij garanderen vermogensbeheerders dat de DeFi-protocollen die zij gebruiken waterdicht zijn."

Vertel ons over Dowsers. Wat doet u precies?

Wij doen formele verificatie voor on-chain finance. Het is het hoogste niveau van softwarebeveiliging dat bestaat — en dat is geen mening, maar een wetenschappelijk feit. Om u een concreet referentiepunt te geven: de drie geautomatiseerde metrolijnen in Parijs zijn formeel geverifieerd voordat ze in gebruik werden genomen. Het oprichtersteam van Dowsers is het team dat dit heeft gedaan, bij RATP. Wij hebben wiskundig bewezen dat software bestaande uit honderdduizenden regels code, die 500 miljoen passagiers per jaar vervoert, geen botsing kon veroorzaken. Daar komen wij vandaan.

Kunt u het concept uitleggen voor iemand die geen ingenieur is?

Formele verificatie werd in de jaren zeventig bedacht. Softwaretesten bestonden toen al, maar hadden een fundamentele beperking: ze konden bugs opsporen, maar niet bewijzen dat ze er niet waren. Wetenschappers — waaronder Edsger Dijkstra en anderen dicht bij Turing — stelden een eenvoudige vraag: wat staat boven informatica? Wiskunde.

Dus creëerden zij deze discipline. U neemt een stuk software, zet het om in een wiskundig model, definieert de risico's die de software nooit mag veroorzaken, en laat een proof engine draaien die elke mogelijke combinatie van instructies onderzoekt. Miljoenen paden. Als geen van deze leidt tot het catastrofale evenement, is de eigenschap bewezen. Als de engine er één vindt, krijgt u het exacte scenario dat de fout zou veroorzaken.

In de context van on-chain finance komen de gevreesde gebeurtenissen neer op drie: een digitaal activum dat wordt opgenomen zonder toestemming van de eigenaar — hetzij door een hacker, hetzij door de ontwikkelaar zelf — een activum dat wordt geblokkeerd zonder dat de gebruiker het weet, of de regels van het protocol die worden gewijzigd zonder hun medeweten.

Dus formele verificatie is een alternatief voor smart contract audits?

Nee, het is een niveau hoger. Een audit is verbeterd testen. Het is noodzakelijk — het maakt de code schoon, spoort bugs op. Maar het bewijst niets. Formele verificatie komt daarna, of parallel, om te bewijzen dat de code niet kan worden aangevallen op specifieke eigenschappen. Wij zitten auditsfirma's niet in de weg. Wij vullen hen aan. Sterker nog, de grootste — Trail of Bits, Halborn, OpenZeppelin, Spearbit — willen formele verificatie gaan integreren in hun aanbod. Zij hebben nog niet de teams om het op onze schaal te doen. Het is een uiterst zeldzame vaardigheid.

Hoe zeldzaam precies?

Er zijn vandaag minder dan 50 mensen wereldwijd die formele verificatie op smart contracts kunnen uitvoeren. De marktleider is een Israëlisch bedrijf, Certora, opgericht in 2017. Zij hebben ongeveer $50 miljoen opgehaald en hebben veertig tot vijftig specialisten. Zij hebben hun eigen proof engine ontwikkeld, recent open source gemaakt — zeer uitgebreid maar zeer complex om te configureren. Hun traditionele businessmodel is in wezen: u bent een groot protocol met $500 miljoen in TVL, u heeft absoluut formele verificatie nodig, hier is onze prijs. Een prijs die zich niet leent voor brede adoptie. Er is ook Runtime Verification in Chicago, ongeveer tien mensen. Dat is het ongeveer.

Wat is dan het waardevoorstel van Dowsers vergeleken met Certora?

Drie woorden: toegankelijkheid, betaalbaarheid, schaalbaarheid. Certora heeft iets opmerkelijks gebouwd, maar exclusief. Wij willen dat formele verificatie een standaard wordt — geen luxe voorbehouden aan protocollen die het zich kunnen veroorloven. We weten dat Morpho twee jaar geleden meer dan een miljoen euro aan audits heeft uitgegeven. Wij zijn nu al goedkoper dan een standaard audit, met een dekkingsniveau dat in een geheel andere klasse zit.

En hier is ons model: zodra u formele verificatie heeft opgezet op uw eerste smart contract, zijn volgende iteraties vrijwel geautomatiseerd. Het eerste project vereist initieel werk — wij begrijpen uw risico's, definiëren samen wat u wilt beschermen, coderen de eigenschappen. Daarna, wanneer het contract evolueert, wordt dat voorbereidende werk hergebruikt. De kosten dalen bij elke iteratie. Dat bedoelen we met schaalbaarheid.

Wie zijn de klanten waarop u zich richt?

Aan de ene kant de code-eigenaren: DeFi- of TradFi-protocolontwikkelaars die willen bewijzen dat hun code veilig is vóór implementatie. Wij tonen hen de exacte regels die risico creëren, en leveren een wiskundig bewijs dat de kritieke eigenschappen niet kunnen worden geschonden.

Aan de andere kant de codegebruikers: asset managers, toezichthouders, institutionele partijen die onafhankelijke due diligence willen uitvoeren op een protocol waarin ze overwegen te investeren — of dat ze al gebruiken. Voor hen beoordelen wij niet de waarde van het protocol. Wij zeggen niet of het zal stijgen of dalen. Wij leveren een wiskundig oordeel over de betrouwbaarheid van de code. De output verschilt per profiel, maar het platform is hetzelfde.

Dat tweede gebruiksscenario roept een vraag op: als u de code van een protocol analyseert namens een derde partij, zonder toestemming van de ontwikkelaar, hoe regelt u dat juridisch?

Zeer zorgvuldig. Ten eerste werken wij alleen met geïdentificeerde entiteiten — KYB is verplicht. Vervolgens ondertekent elke klant die een analyse bestelt twee verbintenissen: een verbod op het gebruik van de resultaten voor offensieve doeleinden, en een overeenkomst dat wij, in geval van een juridisch onderzoek, aan de autoriteiten de lijst van entiteiten die toegang hadden tot die analyses zouden verstrekken. Wij werken samen met toezichthouders. En als wij een kritieke fout in een protocol vinden, informeren wij de ontwikkelaar. Wij doen niet aan ethisch hacken, laat staan afpersing. Wij doen onafhankelijke analyse. Onze missie is vertrouwen in code herstellen — niet het uitbuiten ervan.

Zou een asset manager zoals Franklin Templeton vandaag bij u terecht kunnen?

Ja, op dit moment. Wij hebben vorig jaar al aanvragen in die richting ontvangen van grote asset managers. Het aanbod is gestructureerd, getest, en wij hebben een belangrijk operationeel voordeel: wij werken nooit met de originele code. Wij maken een kopie, zetten die om in een wiskundig model, en draaien simulaties op onze eigen servers. Wij zitten niet in het protocol; wij hebben geen interactie met de chain. Dat is een punt dat wij aan de Europese Commissie hebben kunnen uitleggen, en het neemt direct alle vragen over aansprakelijkheid of inmenging weg.

"Wat wij bieden is gedocumenteerde, traceerbare en wiskundig onderbouwde risicodekking"

In dat verband — wat is uw juridische aansprakelijkheid als een fout die u niet heeft ontdekt achteraf wordt uitgebuit?

Dat is een terechte vraag. Wij werken volgens de Europese norm ISO 17020, die software-evaluatie door een onafhankelijke expert regelt. Het kader rust op een eenvoudig principe: de uitlegbaarheid van de methode. Wij garanderen nooit absolute, 100% onkwetsbaarheid — en dat zeggen wij heel duidelijk tegen onze klanten. Een formele proof engine kan uren, dagen draaien, miljoenen paden verkennen. Het kan er geen oneindig aantal verkennen. Wij documenteren precies de gemaakte aannames, de geteste eigenschappen, de beperkingen van het model. Als een onafhankelijke expert ons scenario opnieuw uitvoert, komt hij tot dezelfde conclusies. Dat is wat reproduceerbaarheid betekent.

Qua aansprakelijkheid, zolang er geen duidelijke methodologische fout is, bevinden wij ons in een kader vergelijkbaar met dat van grote industriële certificeringsbedrijven. Een 100% garantie bestaat nergens in cybersecurity. Wat wij bieden is gedocumenteerde, traceerbare en wiskundig onderbouwde risicodekking. Er is geen vergelijking met een conventionele audit.

U zegt dat formele verificatie verplicht zal worden voor on-chain finance. Maar dat is vandaag nog niet het geval…

Nog niet in de wet, nee. Maar de regulatoire signalen convergeren. De AMF en de ACPR hebben afgelopen april een werkdocument gepubliceerd over protocolcertificering, en wij namen deel als lid van de werkgroep. In dat document wordt formele verificatie geïdentificeerd als het hoogste haalbare zekerheidsniveau in Frankrijk voor on-chain financiële systemen. Wij hebben soortgelijke gesprekken gevoerd met Europese, Amerikaanse en Abu Dhabi-toezichthouders. Het antwoord is altijd hetzelfde: het is de enige aanpak die de afwezigheid van fouten op Wall Street-schaal on-chain kan garanderen.

En er is een nog veelzeggender document: het nationale cybersecurityrapport dat in 2024 door het Witte Huis is gepubliceerd, onderschreven door de CTO van Palantir, de CTO van SAP en het venture fund van de CIA. Formele methoden worden daarin aangemerkt als een Amerikaanse nationale prioriteit. De bewoording is expliciet: deze methoden, uitgevonden in de jaren zeventig, zijn niet ontwikkeld tot het niveau dat ze verdienen, en het is van vitaal belang dat ze schaalbaar worden. Ik ben niet degene die dit zegt — het is het hoofd van de Amerikaanse nationale cybersecurity. Wanneer Wall Street blockchain adopteert als infrastructuur voor financiële transacties, wat al aan de gang is, volgt formele verificatie. Niet over tien jaar. Nu.

Waar staat Dowsers operationeel?

Wij hebben het bedrijf opgericht in de zomer van 2020 en een gestructureerde pre-seed afgerond in 2024. Daarna hebben wij onze seedronde geopend in 2025, met twee fondsen die zijn ingestapt: Orega Cyber Ventures, een Franse cyber VC, als lead, en D-Lab, een Amerikaanse blockchain VC. Onder onze individuele investeerders hebben wij Douglas Levin, oprichter van Black Dog Software, dat hij voor een half miljard dollar heeft verkocht — een van de meest prominente figuren in de Amerikaanse cybersecurity.

En het team?

Wij zijn vandaag met vijftien mensen, met een R&D-hub in Parijs en een uitzonderlijke wetenschappelijke divisie. Onze hoofdonderzoeker wint al tien jaar wereldwijde prijzen voor open-source formele proof engines. Dat is geen detail. Wij hebben een vlaggenschipproject aangekondigd: wij hebben gewerkt voor de ADI Foundation in Abu Dhabi, samen met OpenZeppelin, die de audit verzorgde terwijl wij de formele verificatie deden. In de VS hebben wij aan belangrijke projecten gewerkt met grote spelers in het audit-ecosysteem. Maar wij zijn onder de radar gebleven — zoals iedereen doet bij het opbouwen van de eerste referenties. De Series A markeert het einde van die fase. Wij openen een kantoor in New York, openen een kantoor in Abu Dhabi, en groeien van vijftien naar vijftig mensen. Het doel is een van de wereldleiders te worden in formele verificatie van smart contracts.

Wat is uw visie op de positie van Frankrijk in dit ecosysteem?

Frankrijk heeft een van de beste scholen voor formele verificatie ter wereld. Dat is objectief. Wij hebben buitengewoon talent. Wat wij nog niet hebben, is het vermogen om dat om te zetten in wereldwijde bedrijven. Dat is precies wat wij proberen te doen met Dowsers. Het paradoxale is dat wij beginnen met enkele van de beste experts ter wereld, in een land waar institutionele adoptie achterblijft. Dus richten wij ons direct op Wall Street, Abu Dhabi, Brazilië. Frankrijk zal volgen. Maar het is op dit moment niet onze prioritaire markt.

>> Charles Guillemet (Ledger): "Het vertrouwen in cryptografie is aangetast, blockchains moeten nu migreren"

‍

Patrick Azzopardi, medeoprichter en CEO van Dowsers, betoogt dat wiskundig bewijs van smart contracts binnenkort niet langer optioneel zal zijn voor financiële instellingen. Wij spraken met een voormalig investment banker die nu toonaangevend cybersecurity-ondernemer is geworden..