Case study: Verity end-to-end on Denaria

[denaria-team]

Hi team — we're sharing the results of our first R&D cycle with Verity, and we're writing primarily to open a line of dialogue ahead of the next phase.

Who we are and why we're here

[Denaria](https://docs.denaria.finance/) is a fully-onchain perpetual DEX on Linea, built around a dynamic virtual AMM whose core is pure math — pricing, funding, liquidation. As a foundation we opened an exploratory R&D track to evaluate formal verification as a complement to our audit pipeline, and Verity was the tool that most convinced us on paper. This post is about what happened when we actually put our hands on it.

Two things worth stating upfront, because they frame everything below:

• This is our first real experience with Verity and with Lean 4 at this depth. We're not a formal methods team; we're a DeFi protocol team.
• A meaningful part of the work was done with LLM assistance (Claude Code, specifically). It has been productive, but it also means we may have produced artifacts that look right while missing idioms, conventions, or design intent that an experienced Verity user would spot immediately. This is exactly what we'd like your eyes on.

What we did

We ran a full tracer bullet through Verity on MatrixMath, the signed 2×2 arithmetic library that underpins our dynAMM. Deliverables:

• Lean spec + EDSL implementation side by side
• 14 theorems on MatrixMath (identity, left/right inverse, revert-on-singular, spec conformance, dot-product commutativity) + 17 supporting theorems on a custom SignedInt model as a (Uint256, Bool) pair
• Zero sorry, zero custom axioms
• Yul compiled from the proven EDSL implementation
• Differential fuzz suite (9 tests × 1000 runs) showing bit-for-bit equivalence with our existing Solidity library
• Gas benchmarks against the deployed Solidity

One result we didn't expect: the compiled Yul came out 22–50% cheaper than our hand-written Solidity on 5 of 6 operations, on a per-external-call basis (this is from a preliminary analysis, without concrete production testing yet). We think we understand why — the flat-int256 calling convention skips the ABI encode/decode cost on nested static arrays — but a gut-check from you would be useful.

Where we stand and why we're writing

Overall we're satisfied with the Phase 1 output — the pipeline works, the proofs close, the gas numbers are better than expected. What we need now is not public validation but a sanity check from the people who built Verity, to make sure we're using the tool the way it's meant to be used before we invest in the next phase.

The code (specs, proofs, EDSL implementation, compiled Yul, tests) lives in a private repo of ours. If someone on the team would be willing to take a look, we're happy to share it privately — read-only access to the repo, a walk-through call, or whatever format works for you.

Why timing matters — Phase 2 is CurveMath

The reason we're opening this dialogue now, rather than later, is that the next phase is where verification actually pays off: CurveMath, the library that prices trades on our dynAMM. It's the library called by PerpPair ([verified contract on Lineascan](https://lineascan.build/address/0xb68396dd4230253d27589e2004ac37389836ae17#code)) in the computeShortReturn, computeLongReturn and computeExactAmountInLong functions.

From a formal-verification standpoint it's a substantially harder problem than MatrixMath: the logic solves cubic polynomial equations via Newton's method, with iteration to convergence and all the attendant concerns (bounding the iteration count, guaranteed convergence on the domain of interest, bounds on integer-truncation error, behavior at the edges of the curve parameters). A mistake here isn't academic — it translates directly into a mispriced trade and a loss for LPs or traders.

We already have a fallback plan in mind ("bounded iteration + error bound" if a full-fledged convergence proof turns out to be intractable), but we'd like to understand whether in your experience with Verity there are known patterns, recommended proof techniques, or similar cases you've already tackled. This is exactly the kind of problem where the experience of the people who built the tool is worth far more than any amount of documentation reading.

What we're hoping for from here

An ongoing line of contact as we move into Phase 2. A Discussion thread like this is ideal for async technical exchange; if at some point a call makes sense, we're happy to set one up.

cc @Th0rgal — thank you for building Verity in the open. This post exists because you made that possible.

[fricoben]

Hey !

Thanks for your message, @Th0rgal isn't very active here, sorry about the late response.

We just created a Telegram chat for Verity devs and we'll be much more active there. For a precise Denaria Finance question we could even create a group between our two teams if needed.

See you in the telegram group !

https://t.me/+PHZekKhdjPAxOWU0

[denaria-team]

Hi, thanks a lot for your reply, no worries at all about the delay, we completely understand.

We’ll be very happy to join the Verity devs Telegram group, and we’ll also make sure to share any feedback we think may be useful as we continue with our work.

For the specific Denaria work we’re carrying forward, a dedicated group between the two teams would indeed be the ideal solution for us. As we mentioned, this is still an experimental area for us and we’re not deeply experienced in it yet, so having a technical exchange on proof strategy, constraints, and recommended patterns would be extremely valuable and would help us move forward in the best possible way.

If that works for you, we’d be very happy to proceed in that direction. Thanks again!