We offer a postdoctoral position focused on the formalization of protocols in decentralized finance within the proof assistant Isabelle/HOL, with the goal of developing rigorous theoretical results and certified tools for optimizing decentralized finance transactions.
The position is open within the CAPP group at the Computer Science Laboratory of Grenoble (LIG). The LIG is one of the leading computer science research laboratories in France, located on the University Grenoble Alpes campus, at the foot of the Alps.
The CAPP group research lies at the intersection of logic, programming languages, and proofs.
Automated Market Makers are the cornerstones of Decentralized Finance (DeFi), eliminating the need for traditional order books. In this ecosystem, Liquidity Providers stake tokens to facilitate swaps for Liquidity Takers in exchange for fees.
Concentrated Liquidity Market Makers (CLMMs), introduced by Uniswap v3, have revolutionized this space by allowing providers to allocate liquidity within specific price intervals. This model significantly improves capital efficiency compared to uniform distribution models and has been adopted by several major protocols.
Despite implementation variations (fees, tick spacing), these protocols share core principles. Consequently, liquidity takers often face multiple pools for the same token pair with different characteristics. A critical challenge is to rigorously understand how these pools can be combined, both conceptually and computationally, for liquidity takers to perform transactions with the least slippage (recovering as many tokens as possible in exchange for those they provide).
Decentralized finance refers to a set of peer-to-peer exchange protocols designed to minimize the dependence on intermediaries and central authorities. As DeFi becomes increasingly important in modern economies, establishing rigorous theoretical foundations for its core mechanisms is essential.
The project aims to develop a rigorous formal framework for reasoning about the behavior of Concentrated Liquidity Market Makers and optimizing execution of transactions across multiple pools.
A significant formalization effort regarding the behavior of CLMMs in Isabelle/HOL has already been initiated within the group. The recruited postdoctoral researcher will be responsible for advancing this work. The primary objectives are:
Contract Length: 1 year, renewable for a second year.
Salary: Gross monthly salary between 2900 EUR and 3700 EUR depending on experience.
Start Date: Flexible, as soon as possible.
Interested candidates should send the following documents to:
Mnacho Echenim: mnacho.echenim@univ-grenoble-alpes.fr
Nicolas Peltier: nicolas.peltier@univ-grenoble-alpes.fr