DeFi-csp-models

The repository contains the source code of a Curve Compound Pool model defined in CSP# for PAT.

Compound.csp contains a CSP# implementation of the cUSDC Compound smart contract.

Curve_cPool.csp contains a CSP# definition of Curve.fi: Compound Deposit and Curve.fi: Compound Swap smart contracts.

Tokens.csp is a CSP# implementation of USDC and cCrv (cDAI+cUSDC) tokens.

Model.csp describes behaviors of Curve and Compound users, the analyzed system, and verified properties for both Curve and Compound protocols.

Pat.Lib.Curve.cs implements some of the Curve and Compound mathematical computations in C#.