verified-smart-contracts VS verified-smart-contra

OP, if you are asking about price calculation, IMHO it still follows the original white paper, with many tweaks and improvements, but the fundamental principles remain from V1: https://github.com/runtimeverification/verified-smart-contracts/blob/uniswap/uniswap/x-y-k.pdf (chapter 3) - yes there is something called ticks and virtual liquidity in v3 but those formulas will still give you a good approximation.

You can find the CPMM formulas used by Uniswap here: https://github.com/runtimeverification/verified-smart-contracts/blob/uniswap/uniswap/x-y-k.pdf

This formula can vary with each protocol. For examaple, Maiar DEX uses the industry standard "x*y=k" constant product AMM model, which has proven its reliability in existing implementations, and has been formally modelled and verified. In this formula, k is a fixed constant, meaning the pool’s total liquidity always has to remain the same.

https://github.com/compound-finance/compound-protocol/tree/m...

to this (Uniswap):

https://github.com/runtimeverification/verified-smart-contra...

https://github.com/runtimeverification/verified-smart-contracts/blob/uniswap/uniswap/x-y-k.pdf https://uniswap.org/whitepaper.pdf

Hi, I was going through the formalised explanation of the Constant Product function and it's implementation as per this link. Could you link me to any article that could help me understand the formalisation better.

What is effectively a changelog of features for their new version is probably not the best place to start.

If you'd like to know more then this [0] is a brief summary of Uniswap and this paper [1] is a good introduction to the formalism of the `x * y = k` market making model used by Uniswap.

[0]: https://github.com/runtimeverification/verified-smart-contra...

[q]: https://github.com/runtimeverification/verified-smart-contra...

https://github.com/runtimeverification/verified-smart-contra...

or this (Djed):

https://eprint.iacr.org/2021/1069.pdf

The first just describes the system and then asserts preconditions hold which works well enough for verifying that the code matches the spec but the other actually verify that the spec is doing what the user & developer expect it to by formalising the system and analysing the properties of that system.

Compound's project wouldn't have been vulnerable to any of the attacks executed on CreamFi however they are vulnerable to the class of spec errors. Uniswap and Djed on the other hand would be protected from the majority of that class of issue that Compound experienced. This isn't to say that they are invulnerable but I'd be willing to say that they are approaching "cryptography-grade" security where you can trust these protocols just like you can trust AES, RSA, and ECC encryption & signing.

---

This of course isn't to say that what Compound does is bad but as that incident shows, there is still room for their improvement in the security space. Cryptocurrency and "Decentralised Finance" are finally starting to grow up into proper subsets of the cryptocurrency and game theory communities. Now this might be a bit of general commentary on the SW space but hopefully long term this trend causes some of this security minded design to bleed over into the greater software engineering community.