Erzählen Sie uns von Dowsers. Was genau machen Sie?
Wir führen formale Verifikation für On-Chain-Finanzierungen durch. Es ist das höchste Niveau der Software-Sicherheit, das es gibt — und das ist keine Meinung, sondern eine wissenschaftliche Tatsache. Um Ihnen einen konkreten Bezugspunkt zu geben: Die drei automatisierten U-Bahn-Linien in Paris wurden formal verifiziert, bevor sie in Betrieb genommen wurden. Das Gründungsteam von Dowsers war dasjenige, das dies bei der RATP durchgeführt hat. Wir haben mathematisch bewiesen, dass Software, die aus Hunderttausenden von Codezeilen besteht und 500 Millionen Passagiere pro Jahr befördert, keine Kollision verursachen kann. Daher kommen wir.
Können Sie das Konzept jemandem erklären, der kein Ingenieur ist?
Die formale Verifikation wurde in den 1970er Jahren konzipiert. Softwaretests existierten damals bereits, hatten jedoch eine grundlegende Einschränkung: Sie konnten Fehler erkennen, aber nicht beweisen, dass sie nicht vorhanden waren. Wissenschaftler — darunter Edsger Dijkstra und andere, die Turing nahestanden — stellten eine einfache Frage: Was steht über der Informatik? Die Mathematik.
So entstand diese Disziplin. Man nimmt ein Stück Software, verwandelt es in ein mathematisches Modell, definiert die Risiken, die die Software niemals auslösen darf, und führt eine Beweis-Engine aus, die jede mögliche Kombination von Anweisungen untersucht. Millionen von Pfaden. Wenn keiner von ihnen zum katastrophalen Ereignis führt, ist die Eigenschaft bewiesen. Wenn die Engine einen findet, liefert sie Ihnen das genaue Szenario, das den Fehler auslösen würde.
Im Kontext der On-Chain-Finanzierung reduzieren sich die gefürchteten Ereignisse auf drei: ein digitaler Vermögenswert wird ohne Zustimmung des Eigentümers abgehoben — sei es durch einen Hacker oder den Entwickler selbst —, ein Vermögenswert wird gesperrt, ohne dass der Benutzer es weiß, oder die Regeln des Protokolls werden ohne ihr Wissen geändert.
Ist die formale Verifikation also eine Alternative zu Smart-Contract-Audits?
Nein, es ist eine Stufe darüber. Ein Audit ist ein erweitertes Testen. Es ist notwendig — es bereinigt den Code, entdeckt Fehler. Aber es beweist nichts. Die formale Verifikation kommt danach oder parallel dazu, um zu beweisen, dass der Code in Bezug auf bestimmte Eigenschaften nicht angegriffen werden kann. Wir treten den Audit-Firmen nicht auf die Füße. Wir ergänzen sie. Tatsächlich beginnen die größten — Trail of Bits, Halborn, OpenZeppelin, Spearbit — damit, die formale Verifikation in ihr Angebot integrieren zu wollen. Sie haben noch nicht die Teams, um es in unserem Umfang zu tun. Es ist eine extrem seltene Fähigkeit.
Wie selten genau?
Es gibt heute weltweit weniger als 50 Personen, die formale Verifikation an Smart Contracts durchführen können. Der Marktführer ist ein israelisches Unternehmen, Certora, das 2017 gegründet wurde. Sie haben rund 50 Millionen Dollar aufgebracht und verfügen über vierzig bis fünfzig Spezialisten. Sie haben ihre eigene Beweis-Engine entwickelt, die kürzlich als Open Source veröffentlicht wurde — sehr umfassend, aber sehr komplex zu konfigurieren. Ihr traditionelles Geschäftsmodell ist im Wesentlichen: Sie sind ein großes Protokoll mit 500 Millionen Dollar TVL, Sie benötigen unbedingt eine formale Verifikation, hier ist unser Preis. Ein Preis, der sich nicht für eine breitere Akzeptanz eignet. Es gibt auch Runtime Verification in Chicago, etwa zehn Personen. Das ist ungefähr alles.
Was ist also das Wertversprechen von Dowsers im Vergleich zu Certora?
Drei Worte: Zugänglichkeit, Erschwinglichkeit, Skalierbarkeit. Certora hat etwas Bemerkenswertes geschaffen, aber Exklusives. Wir wollen, dass die formale Verifikation zum Standard wird — kein Luxus, der nur Protokollen vorbehalten ist, die es sich leisten können. Wir wissen, dass Morpho vor zwei Jahren über eine Million Euro für Audits ausgegeben hat. Wir sind bereits günstiger als ein Standard-Audit, mit einem Abdeckungsgrad, der in einer völlig anderen Liga spielt.
Und hier ist unser Modell: Sobald Sie die formale Verifikation für Ihren ersten Smart Contract eingerichtet haben, sind die nachfolgenden Iterationen nahezu automatisiert. Das erste Projekt erfordert Initialisierungsarbeit — wir verstehen Ihre Risiken, definieren mit Ihnen, was Sie schützen möchten, kodieren die Eigenschaften. Danach, wenn sich der Vertrag weiterentwickelt, wird diese Grundlage wiederverwendet. Die Kosten sinken mit jeder Iteration. Das meinen wir mit Skalierbarkeit.
Wer sind die Kunden, die Sie ansprechen?
Auf der einen Seite die Code-Eigentümer: Entwickler von DeFi- oder TradFi-Protokollen, die beweisen möchten, dass ihr Code vor der Bereitstellung sicher ist. Wir zeigen ihnen die genauen Zeilen, die Risiken schaffen, und liefern einen mathematischen Beweis, dass die kritischen Eigenschaften nicht verletzt werden können.
Auf der anderen Seite die Code-Nutzer: Vermögensverwalter, Regulierungsbehörden, institutionelle Akteure, die eine unabhängige Due Diligence für ein Protokoll durchführen möchten, in das sie investieren möchten — oder eines, das sie bereits nutzen. Für sie bewerten wir nicht den Wert des Protokolls. Wir sagen nicht, ob es steigen oder fallen wird. Wir liefern eine mathematische Meinung zur Zuverlässigkeit des Codes. Das Ergebnis unterscheidet sich je nach Profil, aber die Plattform ist dieselbe.
Dieser zweite Anwendungsfall wirft eine Frage auf: Wenn Sie den Code eines Protokolls im Auftrag eines Dritten analysieren, ohne die Zustimmung des Entwicklers, wie gehen Sie damit rechtlich um?
Sehr vorsichtig. Erstens arbeiten wir nur mit identifizierten Einheiten — KYB ist obligatorisch. Dann unterschreibt jeder Kunde, der eine Analyse in Auftrag gibt, zwei Verpflichtungen: ein Verbot, die Ergebnisse für offensive Zwecke zu nutzen, und eine Vereinbarung, dass wir im Falle einer rechtlichen Untersuchung den Behörden die Liste der Entitäten offenlegen würden, die Zugang zu diesen Analysen hatten. Wir kooperieren mit den Regulierungsbehörden. Und wenn wir einen kritischen Fehler in einem Protokoll finden, informieren wir den Entwickler. Wir sind nicht im Geschäft des ethischen Hackings, geschweige denn der Erpressung. Wir führen unabhängige Analysen durch. Unsere Mission ist es, Vertrauen in den Code wiederherzustellen — nicht ihn auszunutzen.
Könnte ein Vermögensverwalter wie Franklin Templeton heute zu Ihnen kommen?
Ja, genau jetzt. Wir haben bereits im letzten Jahr Anfragen dieser Art von großen Vermögensverwaltern erhalten. Das Angebot ist strukturiert, getestet, und wir haben einen wichtigen operativen Vorteil: Wir interagieren niemals mit dem Originalcode. Wir erstellen eine Kopie, verwandeln sie in ein mathematisches Modell und führen Simulationen auf unseren eigenen Servern durch. Wir sind nicht im Protokoll; wir haben keine Interaktion mit der Kette. Das ist ein Punkt, den wir der Europäischen Kommission erklären konnten, und es klärt sofort alle Fragen zur Haftung oder Einmischung.
"Was wir bieten, ist dokumentierte, nachvollziehbare und mathematisch begründete Risikodeckung"
In diesem Zusammenhang — wie sieht Ihre rechtliche Haftung aus, wenn ein von Ihnen nicht erkannter Fehler nachträglich ausgenutzt wird?
Das ist eine berechtigte Frage. Wir arbeiten nach dem europäischen Standard ISO 17020, der die Softwarebewertung durch einen unabhängigen Experten regelt. Der Rahmen basiert auf einem einfachen Prinzip: der Erklärbarkeit der Methode. Wir garantieren niemals absolute, 100%ige Unverwundbarkeit — und das sagen wir unseren Kunden sehr deutlich. Eine formale Beweis-Engine kann stunden-, tagelang laufen und Millionen von Pfaden erkunden. Sie kann nicht eine unendliche Anzahl von ihnen erkunden. Wir dokumentieren genau die gemachten Annahmen, die getesteten Eigenschaften, die Einschränkungen des Modells. Wenn ein unabhängiger Experte unser Szenario erneut abspielt, kommt er zu denselben Schlussfolgerungen. Das bedeutet Reproduzierbarkeit.
In Bezug auf die Haftung, solange kein offensichtlicher methodischer Fehler vorliegt, befinden wir uns in einem Rahmen, der dem großer industrieller Zertifizierungsfirmen ähnelt. Eine 100%ige Garantie gibt es nirgendwo in der Cybersicherheit. Was wir bieten, ist dokumentierte, nachvollziehbare und mathematisch begründete Risikodeckung. Es gibt keinen Vergleich mit einem herkömmlichen Audit.
Sie sagen, die formale Verifikation wird für On-Chain-Finanzierungen obligatorisch werden. Aber das ist heute nicht der Fall…
Noch nicht im Gesetz, nein. Aber die regulatorischen Signale konvergieren. Die AMF und die ACPR haben im letzten April ein Arbeitspapier zur Protokollzertifizierung veröffentlicht, und wir haben als Mitglied der Arbeitsgruppe teilgenommen. In diesem Dokument wird die formale Verifikation als das höchste erreichbare Sicherheitsniveau in Frankreich für On-Chain-Finanzsysteme identifiziert. Wir hatten ähnliche Gespräche mit europäischen, amerikanischen und Abu Dhabi-Regulierungsbehörden. Die Antwort ist immer dieselbe: Es ist der einzige Ansatz, der die Abwesenheit von Fehlern im Maßstab von Wall Street On-Chain garantieren kann.
Und es gibt ein noch aussagekräftigeres Dokument: den nationalen Cybersicherheitsbericht, der 2024 vom Weißen Haus veröffentlicht wurde, unterstützt vom CTO von Palantir, dem CTO von SAP und dem Venture-Fonds der CIA. Formale Methoden werden als nationale Priorität der USA identifiziert. Die Sprache ist eindeutig: Diese in den 70er Jahren erfundenen Methoden wurden nicht auf das Niveau entwickelt, das sie verdienen, und es ist entscheidend, dass sie skalierbar werden. Ich bin nicht derjenige, der das sagt — es ist der Leiter der amerikanischen nationalen Cybersicherheit. Wenn die Wall Street Blockchain als Infrastruktur für Finanztransaktionen übernimmt, was bereits im Gange ist, folgt die formale Verifikation. Nicht in zehn Jahren. Jetzt.
Wo steht Dowsers operativ?
Wir haben das Unternehmen im Sommer 2020 gegründet und 2024 eine strukturierte Pre-Seed-Runde abgeschlossen. Dann haben wir 2025 unsere Seed-Runde eröffnet, mit zwei Fonds, die eingestiegen sind: Orega Cyber Ventures, ein französischer Cyber-VC, als Lead, und D-Lab, ein amerikanischer Blockchain-VC. Unter unseren Einzelinvestoren haben wir Douglas Levin, den Gründer von Black Dog Software, das er für eine halbe Milliarde Dollar verkauft hat — eine der prominentesten Persönlichkeiten in der amerikanischen Cybersicherheit.
Und das Team?
Wir sind heute fünfzehn Personen, mit einem F&E-Zentrum in Paris und einer außergewöhnlichen wissenschaftlichen Abteilung. Unser leitender Forscher hat in den letzten zehn Jahren weltweit Auszeichnungen für Open-Source-Formale Beweis-Engines gewonnen. Das ist kein kleines Detail. Wir haben ein Flaggschiff-Engagement angekündigt: Wir haben für die ADI Foundation in Abu Dhabi gearbeitet, zusammen mit OpenZeppelin, das das Audit durchgeführt hat, während wir die formale Verifikation übernommen haben. In den USA haben wir an bedeutenden Projekten mit großen Akteuren im Audit-Ökosystem gearbeitet. Aber wir sind unter dem Radar geblieben — wie jeder, der seine ersten Referenzen aufbaut. Die Series A markiert das Ende dieser Phase. Wir eröffnen ein Büro in New York, ein Büro in Abu Dhabi und wachsen von fünfzehn auf fünfzig Personen. Das Ziel ist es, einer der globalen Marktführer in der formalen Verifikation von Smart Contracts zu werden.
Wie sehen Sie die Position Frankreichs in diesem Ökosystem?
Frankreich hat eine der besten Schulen für formale Verifikation weltweit. Das ist objektiv. Wir haben außergewöhnliche Talente. Was uns noch fehlt, ist die Fähigkeit, daraus globale Unternehmen zu machen. Genau das versuchen wir mit Dowsers zu erreichen. Das Paradoxe ist, dass wir mit einigen der besten Experten der Welt beginnen, in einem Land, in dem die institutionelle Akzeptanz hinterherhinkt. Also gehen wir direkt nach Wall Street, Abu Dhabi, Brasilien. Frankreich wird nachziehen. Aber es ist nicht unser prioritärer Markt in dieser Phase.
%201.png)
%201.png)
%201.png)
%201.png)
%201.png)
