Patrick Azzopardi (Dowsers): "We guarantee asset managers that the DeFi protocols they use are bulletproof"

Tell us about Dowsers. What exactly do you do?

We do formal verification for on-chain finance. It's the highest level of software security that exists — and that's not an opinion, it's a scientific fact. To give you a concrete reference: the three automated metro lines in Paris were formally verified before they went into service. The founding team at Dowsers is the one that did it, at RATP. We mathematically proved that software made up of hundreds of thousands of lines of code, carrying 500 million passengers a year, could not produce a collision. That's where we come from.

Can you explain the concept for someone who isn't an engineer?

Formal verification was conceptualized in the 1970s. Software testing already existed back then, but it had a fundamental limitation: it could detect bugs, but it couldn't prove they weren't there. Scientists — including Edsger Dijkstra and others close to Turing — asked a simple question: what sits above computer science? Mathematics.

So they created this discipline. You take a piece of software, turn it into a mathematical model, define the risks that software must never trigger, and run a proof engine that explores every possible combination of instructions. Millions of paths. If none of them leads to the catastrophic event, the property is proven. If the engine finds one, it gives you the exact scenario that would trigger the flaw.

In the context of on-chain finance, the dreaded events boil down to three: a digital asset being withdrawn without its owner's consent — whether by a hacker or the developer themselves — an asset being locked without the user knowing, or the protocol's rules being changed without their knowledge.

So formal verification is an alternative to smart contract audits?

No, it's a level above. An audit is enhanced testing. It's necessary — it cleans up the code, catches bugs. But it doesn't prove anything. Formal verification comes in afterward, or in parallel, to prove that the code can't be attacked on specific properties. We're not stepping on audit firms' toes. We complement them. In fact, the biggest ones — Trail of Bits, Halborn, OpenZeppelin, Spearbit — are starting to want to integrate formal verification into their offerings. They don't yet have the teams to do it at our scale. It's an extremely rare skill set.

How rare, exactly?

There are fewer than 50 people in the world today who can perform formal verification on smart contracts. The market leader is an Israeli company, Certora, founded in 2017. They've raised around $50 million and have forty to fifty specialists. They developed their own proof engine, recently open-sourced — very comprehensive but very complex to configure. Their legacy business model is essentially: you're a major protocol with $500 million in TVL, you absolutely need formal verification, here's our price. A price that doesn't lend itself to broader adoption. There's also Runtime Verification in Chicago, about ten people. That's roughly it.

So what's Dowsers' value proposition compared to Certora?

Three words: accessibility, affordability, scalability. Certora built something remarkable, but exclusive. We want formal verification to become a standard — not a luxury reserved for protocols that can afford it. We know Morpho spent over a million euros on audits two years ago. We're already cheaper than a standard audit, with a level of coverage that's in a completely different league.

And here's our model: once you've set up formal verification on your first smart contract, subsequent iterations are nearly automated. The first project requires initialization work — we understand your risks, define with you what you want to protect, code the properties. After that, when the contract evolves, that groundwork gets reused. The cost drops with each iteration. That's what we mean by scalability.

Who are the clients you're targeting?

On one side, the code owners: DeFi or TradFi protocol developers who want to prove their code is safe before deployment. We show them the exact lines creating risk, and we deliver a mathematical proof that the critical properties can't be violated.

On the other side, the code users: asset managers, regulators, institutional players who want to run independent due diligence on a protocol they're considering investing in — or one they're already using. For them, we don't judge the protocol's value. We don't say whether it'll go up or down. We deliver a mathematical opinion on the reliability of the code. The output differs depending on the profile, but the platform is the same.

That second use case raises a question: if you're analyzing a protocol's code on behalf of a third party, without the developer's consent, how do you handle that legally?

Very carefully. First, we only work with identified entities — KYB is mandatory. Then, every client who commissions an analysis signs two commitments: a prohibition on using the results for offensive purposes, and an agreement that, in the event of a legal investigation, we would disclose to authorities the list of entities that had access to those analyses. We cooperate with regulators. And if we find a critical flaw in a protocol, we inform the developer. We're not in the business of ethical hacking, let alone extortion. We do independent analysis. Our mission is to restore trust in code — not exploit it.

Could an asset manager like Franklin Templeton come to you today?

Yes, right now. We already received inquiries along those lines last year from major asset managers. The offering is structured, tested, and we have an important operational advantage: we never interact with the original code. We make a copy, transform it into a mathematical model, and run simulations on our own servers. We're not inside the protocol; we have no interaction with the chain. That's a point we've had the opportunity to explain to the European Commission, and it immediately clears up any questions about liability or interference.

"What we offer is documented, traceable, and mathematically justified risk coverage"

On that note — what's your legal liability if a flaw you didn't catch gets exploited after the fact?

It's a fair question. We operate under the European standard ISO 17020, which governs software evaluation by an independent expert. The framework rests on a simple principle: the explainability of the method. We never guarantee absolute, 100% invulnerability — and we say that very clearly to our clients. A formal proof engine can run for hours, days, exploring millions of paths. It can't explore an infinite number of them. We document precisely the assumptions made, the properties tested, the model's limitations. If an independent expert replays our scenario, they reach the same conclusions. That's what reproducibility means.

In terms of liability, as long as there's no obvious methodological error, we're in a framework similar to that of major industrial certification firms. A 100% guarantee doesn't exist anywhere in cybersecurity. What we offer is documented, traceable, and mathematically justified risk coverage. There's no comparison with a conventional audit.

You say formal verification will become mandatory for on-chain finance. But that's not the case today…

Not yet in the law, no. But the regulatory signals are converging. The AMF and the ACPR published a working paper last April on protocol certification, and we participated as a member of the working group. In that document, formal verification is identified as the highest achievable level of assurance in France for on-chain financial systems. We've had similar conversations with European, American, and Abu Dhabi regulators. The answer is always the same: it's the only approach that can guarantee the absence of flaws at the scale of Wall Street on-chain.

And there's an even more telling document: the national cybersecurity report published by the White House in 2024, endorsed by Palantir's CTO, SAP's CTO, and the CIA's venture fund. Formal methods are identified as a U.S. national priority. The language is explicit: these methods, invented in the '70s, haven't been developed to the level they deserve, and it's vital they become scalable. I'm not the one saying this — it's the head of American national cybersecurity. When Wall Street adopts blockchain as financial transaction infrastructure, which is already underway, formal verification follows. Not in ten years. Now.

Where does Dowsers stand operationally?

We founded the company in the summer of 2020 and closed a structured pre-seed in 2024. Then we opened our seed round in 2025, with two funds coming in: Orega Cyber Ventures, a French cyber VC, as lead, and D-Lab, an American blockchain VC. Among our individual investors, we have Douglas Levin, founder of Black Dog Software, which he sold for half a billion dollars — one of the most prominent figures in American cybersecurity.

And the team?

We're fifteen people today, with an R&D hub in Paris and an exceptional scientific division. Our lead researcher has been winning global awards for open-source formal proof engines for the past decade. That's not a minor detail. We've announced a flagship engagement: we worked for the ADI Foundation in Abu Dhabi, alongside OpenZeppelin, which handled the audit while we handled formal verification. In the U.S., we've worked on significant projects with major players in the audit ecosystem. But we've stayed under the radar — as everyone does when building their first references. The Series A marks the end of that phase. We're opening an office in New York, opening an office in Abu Dhabi, and growing from fifteen to fifty people. The goal is to become one of the global leaders in smart contract formal verification.

What's your take on France's position in this ecosystem?

France has one of the best formal verification schools in the world. That's objective. We have extraordinary talent. What we don't have yet is the ability to turn that into global companies. That's exactly what we're trying to do with Dowsers. The paradox is that we're starting with some of the best experts on the planet, in a country where institutional adoption is lagging. So we're going straight for Wall Street, Abu Dhabi, Brazil. France will come around. But it's not our priority market at this stage.

>> Charles Guillemet (Ledger): "Trust in cryptography is eroded, blockchains must migrate now"

‍