Review "What makes Tezos different" page (#481)

* Add link to governance topic

* Remove info about formal verification b/c no one ever talks about it

* Update with info about user delegating and staking

* Mention layer 2

* Enshrined is a good word to use here, not sure about the language

docs/overview/tezos-different.md

@@ -1,26 +1,25 @@
 ---
 title: What makes Tezos different?
 last_update:
-  date: 13 September 2023
+  date: 29 November 2024
 ---
 
 Here are some of the features that make Tezos different from other blockchains:
 
 ## Tezos can upgrade itself
 
-Tezos has a built-in capability to upgrade itself, which allows the network to evolve without requiring a hard fork. Anyone can propose an upgrade to the protocol and have it adopted by the network without compromising the platform's stability or causing fragmentation. This feature allows Tezos to adapt regularly to new technologies and to address user needs rapidly.
+Tezos has a built-in capability to upgrade itself, which allows the network to evolve without requiring a hard fork. Anyone can propose an upgrade to the protocol and have it adopted by the network without compromising the platform's stability or causing fragmentation. This feature allows Tezos to adapt regularly to new technologies and to address user needs rapidly. For more information, see [Governance](/architecture/governance).
 
 ## Everyone can participate in governance
 
 Anyone who holds XTZ — the chain's native token — can propose changes to how Tezos works, such as changes to gas fees and block times, new features such as Smart Rollups, or even major changes like how the consensus mechanism works.
 
-## Formal verification ensures trust and code quality
-
-*Formal verification* is a process that ensures that a smart contract does what it says it does and has no side effects. Formal verification reduces errors, bugs, and security vulnerabilities in contracts and allows users to trust them. For more information, see [Formal Verification](https://opentezos.com/formal-verification) on opentezos.com.
-
 ## Tezos uses proof of stake
 
-The proof-of-stake consensus model eliminates the need for high energy use, making it the "green" choice for blockchains. Instead of competing to achieve consensus as in proof-of-work models, Tezos nodes (called *bakers*) stake Tezos tokens to earn the right to create blocks and receive rewards. Users who want to participate without running a node themselves can delegate tokens to a baker for a share of the rewards. The bakers keep control of their tokens in that they can unstake them later; and delegators keep complete control of their tokens. Tezos's approach to consensus has been described as [Liquid Proof of Stake](https://medium.com/tezos/liquid-proof-of-stake-aec2f7ef1da7).
+The proof-of-stake consensus model eliminates the need for high energy use, making it the "green" choice for blockchains. Instead of competing to achieve consensus as in proof-of-work models, Tezos nodes (called *bakers*) stake Tezos tokens to earn the right to create blocks and receive rewards. Tezos's approach to consensus has been described as [Liquid Proof of Stake](https://medium.com/tezos/liquid-proof-of-stake-aec2f7ef1da7).
+
+Users who want to participate without running a node themselves can delegate and stake tokens to a baker for a share of the baker's rewards. Users retain full control of their delegated and staked tokens; delegated tokens remain liquid and staked tokens are frozen for a short time but remain in the user's account and can be made liquid after a short delay.
+<!-- TODO link to more detailed info about delegating and staking from the non-baker perspective -->
 
 The proof-of-stake model improves scalability and encourages cooperation via incentives. It also increases the cost of 51% attacks and avoids environmentally wasteful proof-of-work. Tezos launched in June 2018 as one of the first major proof-of-stake networks.
 
@@ -29,3 +28,9 @@ For more information about how Tezos handles proof of stake, see https://tezos.g
 ## Tezos accepts multiple languages
 
 Tezos provides a few different languages for developers to choose from, according to their use case, including versions of Python and JavaScript/TypeScript. For more information, see [Languages](/smart-contracts/languages/).
+
+## Tezos has a robust layer 2 ecosystem
+
+Tezos provides tools that allow high scalability on a layer above the primary Tezos blockchain, known as layer 2. [Smart Rollups](/architecture/smart-rollups) can run large amounts of logic and handle large amounts of data in a separate environment without slowing Tezos itself down. The [Data Availability Layer](/architecture/data-availability-layer) provides high-throughput data to Smart Rollups.
+
+The framework for these layer 2 systems is enshrined in the layer 1 protocol. All layer 2 activity is secured by verifiable commitments and attestations on layer 1.