Rephrase overview (#59)

* rephrase overview

* make Foundry clearer

* want to link to KaaS

* de-emphasize kevm

* optimize the description of kaas.

* Update README.md - Easy to Use

Co-authored-by: Palina <[email protected]>

* Update README.md - Trustworthy

Co-authored-by: Palina <[email protected]>

* Update README.md

* ci integration in README

* Update README.md - scalable

* Update README.md's description of Kontrol

Co-authored-by: JianHong Zhao <[email protected]>

* Update "Easy-to-use" bullet point

* Update tagline

* Another update in Kontrol description

* Another update in Kontrol description

* Removing `-` from `User-Friendly`

* Kontrol capitalization fix

---------

Co-authored-by: Palina <[email protected]>

Author: Stevengre

README.md

@@ -1,5 +1,5 @@
 ---
-description: Formally verify smart contracts using the tools you already know
+description: Kontrol your smart contracts with formal verification made simple
 layout:
   title:
     visible: true
@@ -13,16 +13,20 @@ layout:
     visible: true
 ---
 
-# Kontrol
-
 <div data-full-width="true">
 
 <figure><img src=".gitbook/assets/kontrol logo yellow.png" alt=""><figcaption></figcaption></figure>
 
 </div>
 
-[**Kontrol**](https://github.com/runtimeverification/kontrol) combines **KEVM** and [Foundry](https://book.getfoundry.sh/) to grant developers the ability to perform [formal verification](https://en.wikipedia.org/wiki/Formal\_verification) without learning a new language or tool. This is especially useful for those who are not verification engineers. Additionally, developers can leverage Foundry test suites they have already developed and use symbolic execution to increase the level of confidence.
+# Kontrol
+
+[**Kontrol**](https://github.com/runtimeverification/kontrol) is a powerful formal verification tool for EVM smart contracts that makes complex verification easy. Kontrol supports Foundry tests as specifications, which is especially useful for those who are not verification engineers. Additionally, developers can leverage existing Foundry test suites to do formal verification and increase the level of confidence.
+
 
-[**KEVM**](https://github.com/runtimeverification/evm-semantics) is a tool that enables formal verification of smart contracts on the [Ethereum](https://ethereum.org/en/) blockchain. It provides a mathematical foundation for specifying and implementing smart contracts. Developers can use **KEVM** to rigorously reason about the behavior of their smart contracts, ensuring correctness and reducing the likelihood of vulnerabilities in the contract code.
+- **Open Source**: Kontrol is open source under the [BSD-3 Clause License](https://github.com/runtimeverification/kontrol/blob/master/LICENSE). This gives you full kontrol to use, modify, and redistribute it according to your needs.
+- **User Friendly**: Kontrol gives you the advantage of using languages and testing frameworks you’re already familiar with. Kontrol enables developers to write formal specifications as [Foundry](https://book.getfoundry.sh/) tests in [Solidity](https://soliditylang.org). In addition, this allows developers to reuse their existing test suites for formal verification.
+- **Scalable**: Kontrol automatically verifies your contracts against your formal specifications via compositional symbolic execution. It generates proofs during the verification process, allowing you to verify contracts of any size. Additionally, Kontrol enhances efficiency by supporting lemmas, loop invariants, and bounded model checking.
+- **Trustworthy**: Kontrol has a trustworthy mathematical foundation for specifying and verifying smart contracts. It is built on the open-source, validated, and intuitive formal semantics of Ethereum Virtual Machine (EVM) bytecode, [KEVM](https://github.com/runtimeverification/evm-semantics). This provides an additional guarantee that the smart contracts you have verified will demonstrate the exact same behavior when executed by the virtual machine.
 
-[Foundry](https://book.getfoundry.sh/) is a smart contract development toolchain. It manages dependencies, compiles projects, runs tests, facilitates deployments and provides a command-line interface to interact with the chain via [Solidity](https://soliditylang.org/) scripts. If you’re curious about Foundry, have a look at one of our blog posts about it [here](https://runtimeverification.com/blog/foundry-gen-2-of-ethereum-tooling).
+- **CI Integrated**: In addition to running locally, Kontrol can be integrated into your project's CI for continuous assurance, cloud-based verification, and visualization capabilities via [KaaS](https://docs.runtimeverification.com/kaas).