Patrick Azzopardi (Dowsers) : “Nous garantissons aux assets managers que les protocoles DeFi qu’ils utilisent sont fiables”

Présentez-nous Dowsers. Que faites-vous exactement ?

Nous faisons de la vérification formelle appliquée à la finance on-chain. C'est le niveau de sécurité logicielle le plus élevé qui existe. Ce n'est pas un avis, c'est un fait scientifique. Pour vous donner une référence concrète : les trois lignes de métro automatique à Paris ont été vérifiées formellement avant leur mise en service. C'est l'équipe fondatrice de Dowsers qui l'a fait, à la RATP. Nous avons prouvé mathématiquement que des logiciels composés de centaines de milliers de lignes de code, transportant 500 millions de passagers par an, ne pouvaient pas générer de collision. Voilà d'où nous venons.

Expliquez le principe à quelqu'un qui n'est pas ingénieur…

La vérification formelle a été conceptualisée dans les années 1970. Le testing logiciel existait déjà à l'époque, mais il présentait une limite fondamentale : il pouvait détecter des bugs, il était incapable de prouver leur absence. Des scientifiques (dont Edsger Dijkstra et d'autres proches de Turing) ont alors posé une question simple : qu'est-ce qui est au-dessus de l'informatique ? Les mathématiques.

Ils ont donc créé cette discipline : je prends un logiciel, je le transforme en modèle mathématique, je définis les risques que ce logiciel ne doit jamais provoquer, et je fais tourner un moteur de preuves qui explore toutes les combinaisons possibles d'instructions. Des millions de chemins. Si aucun d'entre eux ne conduit à l'événement catastrophique, la propriété est prouvée. Si le moteur en trouve un, il vous donne l'exemple exact qui permet de déclencher la faille.

Dans le cadre de la finance on-chain, les événements redoutés sont au nombre de trois : qu'un actif numérique soit prélevé sans le consentement de son propriétaire (que ce soit par un hacker ou par le développeur lui-même), qu'il soit bloqué sans que l'utilisateur le sache, ou que les règles du protocole soient modifiées à son insu.

La vérification formelle, c'est donc une alternative aux audits de smart contracts ?

Non, c'est un niveau supérieur. L'audit, c'est du testing amélioré. C'est nécessaire, ça nettoie le code, ça détecte des bugs. Mais ça ne prouve rien. La vérification formelle arrive ensuite, ou en parallèle, pour prouver que le code ne peut pas être attaqué sur des propriétés précises. Nous ne marchons pas sur les plates-bandes des sociétés d'audit. Nous les complétons. D'ailleurs, les plus grandes d'entre elles (Trail of Bits, Halborn, OpenZeppelin, Spearbit) commencent à vouloir intégrer la vérification formelle dans leurs offres. Elles n'ont pas encore les équipes pour le faire à notre échelle. C'est une compétence rarissime.

Rarissime à quel point ?

Il y a aujourd'hui moins de 50 personnes dans le monde capables d'opérer de la vérification formelle sur des smart contracts. Le leader du marché est une société israélienne, Certora, fondée en 2017, qui a levé environ 50 millions de dollars et dispose d'une quarantaine à cinquantaine de spécialistes. Ils ont développé leur propre moteur de preuves, mis en open source récemment, très complet mais très complexe à paramétrer. Leur modèle économique historique, c'est : vous êtes un grand protocole avec 500 millions de TVL, vous avez absolument besoin de vérification formelle, voici notre tarif. Un tarif qui ne permet pas la démocratisation. Il y a aussi Runtime Verification, à Chicago, une dizaine de personnes. C'est à peu près tout.

Quelle est alors la proposition de valeur de Dowsers par rapport à Certora ?

Trois mots : accessibilité, affordability, scalabilité. Certora a construit quelque chose de remarquable, mais d'exclusif. Nous, on veut que la vérification formelle devienne un standard, pas un luxe réservé aux protocoles qui ont les moyens de se l'offrir. On sait que Morpho a dépensé plus d'un million d'euros en audits il y a deux ans. Nous sommes déjà moins chers qu'un audit standard pour un niveau de couverture sans commune mesure.

Et notre modèle, c'est qu'une fois que vous avez paramétré la vérification formelle sur votre premier smart contract, les évolutions suivantes sont quasi-automatisées. Le premier projet nécessite un travail d'initialisation : on comprend vos risques, on définit avec vous ce que vous voulez protéger, on code les propriétés. Ensuite, quand le contrat évolue, cette préparation est réutilisée. Le coût diminue à chaque itération. C'est ce qu'on appelle la scalabilité.

Quels sont les clients que vous visez ?

D'un côté, les owners du code : développeurs de protocoles DeFi ou TradFi qui veulent prouver que leur code est sûr avant déploiement. On leur indique les lignes précises qui créent un risque, et on leur délivre une preuve mathématique que les propriétés critiques ne peuvent pas être violées.

De l'autre côté, les users du code : asset managers, régulateurs, institutionnels qui veulent faire une due diligence indépendante sur un protocole dans lequel ils envisagent d'investir ou qu'ils utilisent déjà. Pour eux, on ne juge pas la valeur du protocole, on ne dit pas s'il va monter ou baisser. On délivre un avis mathématique sur la fiabilité du code. La sortie est différente selon le profil, mais la plateforme est la même.

Ce deuxième cas soulève une question : si vous analysez le code d'un protocole pour le compte d'un tiers, sans l'accord du développeur, comment encadrez-vous ça juridiquement ?

Très rigoureusement. D'abord, nous ne travaillons qu'avec des entités identifiées, KYB obligatoire. Ensuite, tout client qui commande une analyse signe deux engagements : l'interdiction d'exploiter les résultats à des fins offensives, et l'acceptation que, dans le cas d'une investigation légale, nous communiquerions aux autorités la liste des entités ayant eu accès à ces analyses. Nous coopérons avec les régulateurs. Et si nous trouvons une faille critique dans un protocole, nous en informons le développeur. Nous ne sommes pas dans le hack éthique, encore moins dans l'extorsion. Nous sommes dans l'analyse indépendante. Notre mission, c'est de rendre confiance dans le code. Pas de l'exploiter.

Un asset manager comme Franklin Templeton pourrait vous solliciter aujourd'hui ?

Oui, dès maintenant. On a déjà eu des demandes en ce sens l'année dernière de la part de grands asset managers. L'offre est structurée, testée, et nous avons un avantage opérationnel important : nous n'interagissons jamais avec le code original. Nous en faisons une copie, nous la transformons en modèle mathématique, et nous faisons tourner les simulations sur nos propres serveurs. Nous ne sommes pas dans le protocole, nous n'avons aucune interaction avec la chaîne. C'est un point que nous avons eu l'occasion d'expliquer à la Commission européenne, et qui lève immédiatement les questions de responsabilité ou d'ingérence.

“Ce que nous offrons, c'est une couverture de risque documentée, traçable et mathématiquement justifiée”

Justement, quelle est votre responsabilité juridique si une faille que vous n'avez pas détectée est exploitée après coup ?

C'est une question légitime. Nous opérons dans le cadre de la norme européenne ISO 17020, qui régit l'évaluation logicielle par un expert indépendant. Ce cadre repose sur un principe simple : l'explicabilité de la méthode. Nous ne garantissons jamais une invulnérabilité absolue à 100 %, et nous le disons très clairement à nos clients. Un moteur de preuves formelles peut tourner des heures, des jours, explorer des millions de chemins. Il ne peut pas en explorer une infinité. Nous documentons précisément les hypothèses prises, les propriétés testées, les limitations du modèle. Si un expert indépendant rejoue notre scénario, il arrive aux mêmes conclusions. C'est ce qu'on appelle la reproductibilité.

En termes de responsabilité, tant qu'il n'y a pas d'erreur manifeste de méthode, nous sommes dans un cadre similaire à celui des grands cabinets de certification industrielle. La garantie à 100 % n'existe nulle part en cybersécurité. Ce que nous offrons, c'est une couverture de risque documentée, traçable et mathématiquement justifiée. C'est sans comparaison avec un audit classique.

Vous dites que la vérification formelle va devenir obligatoire pour la finance on-chain. Mais aujourd'hui, ce n'est pas le cas…

Pas encore dans la loi, effectivement. Mais les signaux réglementaires convergent. L'AMF et l'ACPR ont publié en avril dernier un working paper sur la certification des protocoles, dans lequel nous avons participé en tant que membre du groupe de travail. Dans ce document, la vérification formelle est identifiée comme le plus haut niveau de garantie atteignable en France pour les systèmes financiers on-chain. Nous avons eu des discussions similaires avec des régulateurs européens, américains et à Abu Dhabi. La réponse est toujours la même : c'est la seule approche qui permette de garantir l'absence de failles à l'échelle de Wall Street on-chain.

Et il y a un document encore plus éloquent : le rapport de cybersécurité nationale publié par la Maison-Blanche en 2024, endossé par le CTO de Palantir, le CTO de SAP et le fonds de la CIA. Les formal methods sont identifiées comme une priorité nationale américaine. Le texte est explicite : ces méthodes inventées dans les années 70 n'ont pas été développées au niveau qu'elles méritent, et il est vital qu'elles deviennent scalables. Ce n'est pas moi qui le dis, c'est le patron de la cybersécurité nationale américaine. Quand Wall Street adopte la blockchain comme infrastructure de transaction financière, ce qui est en cours, la vérification formelle suit. Pas dans dix ans. Maintenant.

Où en est Dowsers opérationnellement ?

Nous avons créé l'entreprise à l'été 2020 et réussi un pré-seed structuré en 2024. Et nous ensuite avons ouvert notre seed en 2025, avec l'entrée de deux fonds : Orega Cyber Ventures, un VC cyber français, en lead, et D-Lab, un VC blockchain américain. Du côté des investisseurs individuels, nous avons notamment Douglas Levin, fondateur de Black Dog Software, qu'il a cédé pour un demi-milliard de dollars, et qui est l'une des figures emblématiques de la cybersécurité américaine.

Et l’équipe ?

Nous avons une équipe de quinze personnes aujourd'hui, avec un pôle R&D à Paris et un pôle scientifique d'exception. Notre chercheur principal remporte depuis dix ans les prix mondiaux sur les moteurs de preuves formelles open source. Ce n'est pas un détail. Nous avons une mission emblématique annoncée : nous avons travaillé pour la fondation ADI à Abu Dhabi, en parallèle d'OpenZeppelin qui gérait l'audit, nous faisions la vérification formelle. Aux États-Unis, nous avons travaillé sur des sujets significatifs avec des acteurs importants de l'écosystème d'audit. Mais nous sommes restés discrets, comme le font tous ceux qui construisent leurs premières références. La Série A, c'est la fin de cette phase. Ouverture d'un bureau à New York, ouverture d'un bureau à Abu Dhabi, passage de quinze à cinquante personnes. L'objectif, c'est d'être l'un des leaders mondiaux de la vérification formelle de smart contracts.

Que pensez-vous du positionnement français dans cet écosystème ?

La France a une école de vérification formelle parmi les meilleures au monde. C'est objectif. Nous avons des talents extraordinaires. Ce qu'on n'a pas encore, c'est la capacité à les transformer en entreprises globales. C'est exactement ce que nous essayons de faire avec Dowsers. Le paradoxe, c'est qu'on part avec parmi les meilleurs experts au monde, dans un pays où l'adoption institutionnelle est en retard. Donc on vise directement Wall Street, Abu Dhabi, le Brésil. La France viendra. Mais ce n'est pas notre marché prioritaire au stade où nous en sommes.

>> Charles Guillemet (Ledger) : “La confiance dans la cryptographie est érodée, il faut migrer les blockchains maintenant”

‍

‍

Présentez-nous Dowsers. Que faites-vous exactement ?

Nous faisons de la vérification formelle appliquée à la finance on-chain. C'est le niveau de sécurité logicielle le plus élevé qui existe. Ce n'est pas un avis, c'est un fait scientifique. Pour vous donner une référence concrète : les trois lignes de métro automatique à Paris ont été vérifiées formellement avant leur mise en service. C'est l'équipe fondatrice de Dowsers qui l'a fait, à la RATP. Nous avons prouvé mathématiquement que des logiciels composés de centaines de milliers de lignes de code, transportant 500 millions de passagers par an, ne pouvaient pas générer de collision. Voilà d'où nous venons.

Expliquez le principe à quelqu'un qui n'est pas ingénieur…

La vérification formelle a été conceptualisée dans les années 1970. Le testing logiciel existait déjà à l'époque, mais il présentait une limite fondamentale : il pouvait détecter des bugs, il était incapable de prouver leur absence. Des scientifiques (dont Edsger Dijkstra et d'autres proches de Turing) ont alors posé une question simple : qu'est-ce qui est au-dessus de l'informatique ? Les mathématiques.

Ils ont donc créé cette discipline : je prends un logiciel, je le transforme en modèle mathématique, je définis les risques que ce logiciel ne doit jamais provoquer, et je fais tourner un moteur de preuves qui explore toutes les combinaisons possibles d'instructions. Des millions de chemins. Si aucun d'entre eux ne conduit à l'événement catastrophique, la propriété est prouvée. Si le moteur en trouve un, il vous donne l'exemple exact qui permet de déclencher la faille.

Dans le cadre de la finance on-chain, les événements redoutés sont au nombre de trois : qu'un actif numérique soit prélevé sans le consentement de son propriétaire (que ce soit par un hacker ou par le développeur lui-même), qu'il soit bloqué sans que l'utilisateur le sache, ou que les règles du protocole soient modifiées à son insu.

La vérification formelle, c'est donc une alternative aux audits de smart contracts ?

Non, c'est un niveau supérieur. L'audit, c'est du testing amélioré. C'est nécessaire, ça nettoie le code, ça détecte des bugs. Mais ça ne prouve rien. La vérification formelle arrive ensuite, ou en parallèle, pour prouver que le code ne peut pas être attaqué sur des propriétés précises. Nous ne marchons pas sur les plates-bandes des sociétés d'audit. Nous les complétons. D'ailleurs, les plus grandes d'entre elles (Trail of Bits, Halborn, OpenZeppelin, Spearbit) commencent à vouloir intégrer la vérification formelle dans leurs offres. Elles n'ont pas encore les équipes pour le faire à notre échelle. C'est une compétence rarissime.

Rarissime à quel point ?

Il y a aujourd'hui moins de 50 personnes dans le monde capables d'opérer de la vérification formelle sur des smart contracts. Le leader du marché est une société israélienne, Certora, fondée en 2017, qui a levé environ 50 millions de dollars et dispose d'une quarantaine à cinquantaine de spécialistes. Ils ont développé leur propre moteur de preuves, mis en open source récemment, très complet mais très complexe à paramétrer. Leur modèle économique historique, c'est : vous êtes un grand protocole avec 500 millions de TVL, vous avez absolument besoin de vérification formelle, voici notre tarif. Un tarif qui ne permet pas la démocratisation. Il y a aussi Runtime Verification, à Chicago, une dizaine de personnes. C'est à peu près tout.

Quelle est alors la proposition de valeur de Dowsers par rapport à Certora ?

Trois mots : accessibilité, affordability, scalabilité. Certora a construit quelque chose de remarquable, mais d'exclusif. Nous, on veut que la vérification formelle devienne un standard, pas un luxe réservé aux protocoles qui ont les moyens de se l'offrir. On sait que Morpho a dépensé plus d'un million d'euros en audits il y a deux ans. Nous sommes déjà moins chers qu'un audit standard pour un niveau de couverture sans commune mesure.

Et notre modèle, c'est qu'une fois que vous avez paramétré la vérification formelle sur votre premier smart contract, les évolutions suivantes sont quasi-automatisées. Le premier projet nécessite un travail d'initialisation : on comprend vos risques, on définit avec vous ce que vous voulez protéger, on code les propriétés. Ensuite, quand le contrat évolue, cette préparation est réutilisée. Le coût diminue à chaque itération. C'est ce qu'on appelle la scalabilité.

Quels sont les clients que vous visez ?

D'un côté, les owners du code : développeurs de protocoles DeFi ou TradFi qui veulent prouver que leur code est sûr avant déploiement. On leur indique les lignes précises qui créent un risque, et on leur délivre une preuve mathématique que les propriétés critiques ne peuvent pas être violées.

De l'autre côté, les users du code : asset managers, régulateurs, institutionnels qui veulent faire une due diligence indépendante sur un protocole dans lequel ils envisagent d'investir ou qu'ils utilisent déjà. Pour eux, on ne juge pas la valeur du protocole, on ne dit pas s'il va monter ou baisser. On délivre un avis mathématique sur la fiabilité du code. La sortie est différente selon le profil, mais la plateforme est la même.

Ce deuxième cas soulève une question : si vous analysez le code d'un protocole pour le compte d'un tiers, sans l'accord du développeur, comment encadrez-vous ça juridiquement ?

Très rigoureusement. D'abord, nous ne travaillons qu'avec des entités identifiées, KYB obligatoire. Ensuite, tout client qui commande une analyse signe deux engagements : l'interdiction d'exploiter les résultats à des fins offensives, et l'acceptation que, dans le cas d'une investigation légale, nous communiquerions aux autorités la liste des entités ayant eu accès à ces analyses. Nous coopérons avec les régulateurs. Et si nous trouvons une faille critique dans un protocole, nous en informons le développeur. Nous ne sommes pas dans le hack éthique, encore moins dans l'extorsion. Nous sommes dans l'analyse indépendante. Notre mission, c'est de rendre confiance dans le code. Pas de l'exploiter.

Un asset manager comme Franklin Templeton pourrait vous solliciter aujourd'hui ?

Oui, dès maintenant. On a déjà eu des demandes en ce sens l'année dernière de la part de grands asset managers. L'offre est structurée, testée, et nous avons un avantage opérationnel important : nous n'interagissons jamais avec le code original. Nous en faisons une copie, nous la transformons en modèle mathématique, et nous faisons tourner les simulations sur nos propres serveurs. Nous ne sommes pas dans le protocole, nous n'avons aucune interaction avec la chaîne. C'est un point que nous avons eu l'occasion d'expliquer à la Commission européenne, et qui lève immédiatement les questions de responsabilité ou d'ingérence.

“Ce que nous offrons, c'est une couverture de risque documentée, traçable et mathématiquement justifiée”

Justement, quelle est votre responsabilité juridique si une faille que vous n'avez pas détectée est exploitée après coup ?

C'est une question légitime. Nous opérons dans le cadre de la norme européenne ISO 17020, qui régit l'évaluation logicielle par un expert indépendant. Ce cadre repose sur un principe simple : l'explicabilité de la méthode. Nous ne garantissons jamais une invulnérabilité absolue à 100 %, et nous le disons très clairement à nos clients. Un moteur de preuves formelles peut tourner des heures, des jours, explorer des millions de chemins. Il ne peut pas en explorer une infinité. Nous documentons précisément les hypothèses prises, les propriétés testées, les limitations du modèle. Si un expert indépendant rejoue notre scénario, il arrive aux mêmes conclusions. C'est ce qu'on appelle la reproductibilité.

En termes de responsabilité, tant qu'il n'y a pas d'erreur manifeste de méthode, nous sommes dans un cadre similaire à celui des grands cabinets de certification industrielle. La garantie à 100 % n'existe nulle part en cybersécurité. Ce que nous offrons, c'est une couverture de risque documentée, traçable et mathématiquement justifiée. C'est sans comparaison avec un audit classique.

Vous dites que la vérification formelle va devenir obligatoire pour la finance on-chain. Mais aujourd'hui, ce n'est pas le cas…

Pas encore dans la loi, effectivement. Mais les signaux réglementaires convergent. L'AMF et l'ACPR ont publié en avril dernier un working paper sur la certification des protocoles, dans lequel nous avons participé en tant que membre du groupe de travail. Dans ce document, la vérification formelle est identifiée comme le plus haut niveau de garantie atteignable en France pour les systèmes financiers on-chain. Nous avons eu des discussions similaires avec des régulateurs européens, américains et à Abu Dhabi. La réponse est toujours la même : c'est la seule approche qui permette de garantir l'absence de failles à l'échelle de Wall Street on-chain.

Et il y a un document encore plus éloquent : le rapport de cybersécurité nationale publié par la Maison-Blanche en 2024, endossé par le CTO de Palantir, le CTO de SAP et le fonds de la CIA. Les formal methods sont identifiées comme une priorité nationale américaine. Le texte est explicite : ces méthodes inventées dans les années 70 n'ont pas été développées au niveau qu'elles méritent, et il est vital qu'elles deviennent scalables. Ce n'est pas moi qui le dis, c'est le patron de la cybersécurité nationale américaine. Quand Wall Street adopte la blockchain comme infrastructure de transaction financière, ce qui est en cours, la vérification formelle suit. Pas dans dix ans. Maintenant.

Où en est Dowsers opérationnellement ?

Nous avons créé l'entreprise à l'été 2020 et réussi un pré-seed structuré en 2024. Et nous ensuite avons ouvert notre seed en 2025, avec l'entrée de deux fonds : Orega Cyber Ventures, un VC cyber français, en lead, et D-Lab, un VC blockchain américain. Du côté des investisseurs individuels, nous avons notamment Douglas Levin, fondateur de Black Dog Software, qu'il a cédé pour un demi-milliard de dollars, et qui est l'une des figures emblématiques de la cybersécurité américaine.

Et l’équipe ?

Nous avons une équipe de quinze personnes aujourd'hui, avec un pôle R&D à Paris et un pôle scientifique d'exception. Notre chercheur principal remporte depuis dix ans les prix mondiaux sur les moteurs de preuves formelles open source. Ce n'est pas un détail. Nous avons une mission emblématique annoncée : nous avons travaillé pour la fondation ADI à Abu Dhabi, en parallèle d'OpenZeppelin qui gérait l'audit, nous faisions la vérification formelle. Aux États-Unis, nous avons travaillé sur des sujets significatifs avec des acteurs importants de l'écosystème d'audit. Mais nous sommes restés discrets, comme le font tous ceux qui construisent leurs premières références. La Série A, c'est la fin de cette phase. Ouverture d'un bureau à New York, ouverture d'un bureau à Abu Dhabi, passage de quinze à cinquante personnes. L'objectif, c'est d'être l'un des leaders mondiaux de la vérification formelle de smart contracts.

Que pensez-vous du positionnement français dans cet écosystème ?

La France a une école de vérification formelle parmi les meilleures au monde. C'est objectif. Nous avons des talents extraordinaires. Ce qu'on n'a pas encore, c'est la capacité à les transformer en entreprises globales. C'est exactement ce que nous essayons de faire avec Dowsers. Le paradoxe, c'est qu'on part avec parmi les meilleurs experts au monde, dans un pays où l'adoption institutionnelle est en retard. Donc on vise directement Wall Street, Abu Dhabi, le Brésil. La France viendra. Mais ce n'est pas notre marché prioritaire au stade où nous en sommes.

>> Charles Guillemet (Ledger) : “La confiance dans la cryptographie est érodée, il faut migrer les blockchains maintenant”

‍