Merge pull request #22 from albist/morphogpt-doc-update

Morphogpt doc update

documents/articles/mirror-Formally_Verifying_Blue_Certora.md

@@ -0,0 +1,31 @@
+Link: https://morpho.mirror.xyz/pk_jXDlq-pv8TcHeN7X4-zZcYa7TLRmgv87UBCjG4i8
+Title: Formally Verifying Morpho Blue with Certora
+
+Formally Verifying Morpho Blue with Certora
+21 december 2023
+Morpho Labs
+
+Led by Quentin Garchery (https://twitter.com/Q_Garchery), the formal verification of Morpho Blue involved collaboration with other companies and individuals. Morpho Labs would like to thank members of Certora (https://www.certora.com/), specifically Jochen Hoenicke (https://jochen-hoenicke.de/), and Daejun Park (https://twitter.com/daejunpark) from a16z (https://twitter.com/a16zcrypto) for their contributions.
+
+
+Designed as a base layer for decentralized lending, software correctness and security are paramount for Morpho Blue.
+Ensuring this involves a multi-faceted process across several phases, from pre-build to post-deployment. However, when proving the correctness of a smart contract, it is hard to find a method more rigorous and comprehensive than formal verification.
+Used effectively, formal verification can help develop higher quality and, most importantly, more secure code. That is why Morpho Labs, with help from members of Certora and a16z, have invested significant time and resources into formally verifying Morpho Blue.
+This article introduces formal verification, explains why it is suited to Morpho Blue, and demonstrates how it has been used to secure the protocol.
+The full scope of Morpho Blue’s formal verification is available at this link: https://github.com/morpho-org/morpho-blue/tree/main/certora.
+
+An introduction to formal verification
+Formal verification (https://en.wikipedia.org/wiki/Formal_verification) is the process of using mathematical methods to prove the correctness of a smart contract by verifying that it satisfies certain properties. These properties are expressed using formal language supported by the verification tool used to prove them.
+In Morpho Blue’s case, specific information was written using CVL (Certora's Verification Language: https://docs.certora.com/en/latest/docs/cvl/index.html) and was verified by the Certora prover.
+Formal verification is a powerful way to evaluate code correctness because it is exhaustive. Other methods, such as unit testing (https://en.wikipedia.org/wiki/Unit_testing), are not. With tests, one can only check for correctness for specific scenarios (some inputs), while formal verification allows one to check for every scenario (all inputs).
+Of course, everything has its pros and cons. Formal verification is comprehensive, but it is also resource-intensive. Its effectiveness depends heavily on the quality of the specifications. For developers, performing formal verification can be time-consuming, and it is often difficult to grasp the concepts that make it work on top of the tools and quirks that may exist.
+
+Formally verifying Morpho Blue
+Many code bases are too complex for formal verification, but Morpho Blue is well suited to it. As mentioned, the process can be time-consuming and only exaggerated by the complexity of a code base. The larger the code base, the more challenging it is to verify. Additionally, past specifications must also be updated if part of the code is upgraded.
+Morpho Blue, however, is neither complex nor upgradeable. Its minimalist, immutable code base, consisting of only 600 lines of code, makes it a good fit for formal verification.
+With that clarification out of the way, two examples are described in the article to demonstrate the verification performed on Morpho Blue.
+
+Understanding the limitations
+Despite the thoroughness of formal verification, it cannot guarantee absolute perfection or eliminate all potential risks associated with Morpho Blue.
+Formal verification is effective within the defined scope of specifications and assumptions. Human input and interpretation, incomplete specifications, and bugs in the tools used can also impact the accuracy of results.
+For more on Morpho Blue’s formal verification, visit the GitHub: https://github.com/morpho-org/morpho-blue/tree/main/certora

documents/articles/mirror-Lido_joins_Morpho_Blue.md

@@ -0,0 +1,44 @@
+Link: https://morpho.mirror.xyz/L0nKnKMgypUXjXWmZRaQa_85KasMgJXT91Zw_iOqZjE
+Title: Lido joins the Morpho Blue ecosystem and supports stETH markets
+
+Lido joins the Morpho Blue ecosystem and supports stETH markets
+15 December 2023
+Morpho Labs
+
+Lido DAO’s Liquidity Observation Lab will incentivize stETH (https://help.lido.fi/en/articles/5230610-what-is-steth) markets on Morpho Blue, a new base layer for decentralized lending, to enhance stETH’s capabilities as collateral and increase its adoption.
+stETH is the largest ETH liquid staking token (LST) by market cap (~$21.0B), with its staking rewards and liquidity making it an attractive collateral asset for borrowers. However, its usage remains constrained due to the limitations of existing lending platforms. Morpho Blue is set to change this by providing stETH lending markets more flexibility, efficiency, and resiliency.
+
+Why stETH markets on Morpho Blue
+- Greater efficiency
+Any borrower using stETH as collateral is primarily concerned with maximizing efficiency. The more efficient stETH is as collateral, the more demand there is to use it. This is where Morpho Blue excels:
+  - Higher LTVs: Morpho Blue significantly boosts the capital efficiency of stETH in comparison to AaveV3 offering LTVs up to 98% compared to the 90% on Aave’s eMode.
+  - Lower Borrowing Costs: Morpho Blue is a completely autonomous protocol with no additional maintenance or reserve fees. Along with higher utilization rates (90%) in each market, Morpho Blue can offer borrowers significantly lower borrowing costs.
+  - Reduced Gas Costs: Morpho Blue is a remarkably simple protocol with a much smaller footprint than existing lending platforms - providing stETH as collateral and borrowing ETH consumes 3 to 5 times less gas on Morpho Blue than AaveV3.
+
+- Shared liquidity
+Even though stETH is listed on multiple lending platforms, including Aave, Compound, and Spark, with almost identical risk parameters, they do not share liquidity. As a result, each market has to be bootstrapped individually.
+On Morpho Blue, a single stETH lending market can be used by multiple MetaMorpho Vaults and applications, meaning bootstrapping only has to be done once.
+For example, take two different MetaMorpho vaults. One specializes in lending against LSTs, and the other on blue-chip collateral. Both vaults can end up allocating to the same market with stETH collateral and ETH as the loan asset. Liquidity may enter separate vaults but is aggregated into one stETH market.
+
+- Unlock new use cases
+Traditional lending platforms have built-in risk management where token holders govern new asset listings and risk parameters. Due to the design of lending pools, governance enforces a restrictive one-size-fits-all approach that limits the number of listed assets and imposes caps (https://governance.aave.com/t/gauntlet-methodologies-borrow-and-supply-cap/11487).
+Demand to borrow a broader set of assets against stETH exists, yet it is constrained to the assets listed on current platforms.
+Morpho Blue will unlock new demand for stETH collateral with its highly flexible and permissionless markets. stETH markets can be created with any assets and higher LTVs without the need for governance proposals, approvals, and operations. If a potential use case for stETH needs a lending market, it can be created almost instantaneously.
+Lastly, Morpho Blue’s simple code base can be easily integrated anywhere, allowing for rapid expansion of stETH liquidity.
+
+- Immutable markets
+Having liquidity for an asset is one thing, but ensuring the liquidity is always available is another.
+Traditional lending platforms can modify and even halt markets. When paused, all liquidity is inaccessible by users and can be the case for extended periods.
+In contrast, a Morpho Blue market is similar to a Uniswap v3 pool - immutable and cannot be modified or halted by governance, so liquidity is available in perpetuity.
+Lido DAO aims to provide a secure, decentralized, and trustless staking token (https://blog.lido.fi/the-road-to-trustless-ethereum-staking/). Morpho Blue’s ownerless markets mean liquidity built around stETH shares these values.
+
+
+Bootstrapping long-lasting liquidity
+- Targeted incentives
+Morpho Blue allows users to be more targeted with the use cases they incentivize.
+On current lending platforms, one cannot specifically incentivize the usage of stETH without indirectly benefiting other collateral assets. On Morpho Blue, one can choose to incentivize a specific pair of assets they know has a strong use case, such as an ETH(stETH) market.
+
+- Initial distribution
+The Lido DAO’s Liquidity Observation Lab has committed to supporting bootstrapping markets with stETH as collateral such as ETH(stETH), USDC(stETH), and USDT(stETH).
+The Morpho DAO may also consider contributing with additional incentives and we can expect this to be part of the discussion on the Morpho Forum.
+For more information on Morpho Blue (https://morpho.mirror.xyz/hfVXz323zp9CmJ1PLDL4UhdLITGQ865VIJUyvZYyMA4) and Lido (https://lido.fi/).