doc: add picture of verification techniques

coq/CoqOfSolidity/contracts/tutorial/model.v

@@ -27,7 +27,7 @@ Lemma run_checked_add_t_uint256 codes environment state
 Proof.
   unfold safe_add in H_sum.
   destruct (_ <? _) eqn:? in H_sum; inversion_clear H_sum.
-  unfold Contract_16.Contract_16_deployed.checked_add_t_uint256, safe_add in *.
+  unfold Contract_16.Contract_16_deployed.checked_add_t_uint256.
   lu.
   repeat (lu || cu || p).
   s.

coq/docs/src/SUMMARY.md

@@ -1,5 +1,6 @@
 # Summary
 
+[Presentation](./presentation.md)
 [Introduction](./introduction.md)
 
 # User Guide

coq/docs/src/introduction.md

@@ -1,6 +1,6 @@
 # Introduction
 
-[coq-of-solidity](https://github.com/formal-land/coq-of-solidity) is a tool to formally verify properties about smart contracts written in 🪨 [Solidity](https://soliditylang.org/). Formal verification is about checking properties on a program for _every possible inputs_. This contrasts with testing which only checks a finite amount of cases. It is the most powerful way to ensure your code is bug-free! ✅ It was originally developed for critical software in 🧑‍🚀 space systems, nuclear plants, etc. but it is now becoming more and more popular for the blockchain.
+[coq-of-solidity](https://github.com/formal-land/coq-of-solidity) is a tool to formally verify properties about smart contracts written in 🪨 [Solidity](https://soliditylang.org/). Formal verification is about checking properties on a program for _every possible input_. This contrasts with testing, which only checks a finite number of cases. It is the most powerful way to ensure your code is bug-free! ✅ It was originally developed for critical software in 🧑‍🚀 space systems, nuclear plants, etc. but it is now becoming more and more popular for the blockchain.
 
 > In the rest of the documentation, we assume you have some knowledge in formal verification and in particular in the 🐓 [Coq](https://coq.inria.fr/) proof assistant which we use. On a general note, expect it to be _harder_ to fully formally verify a program than to write it. Still, it must be the _simplest way_ to truly ensure your program is correct.
 
@@ -12,14 +12,17 @@ Thanks to `coq-of-solidity`, you can:
 - Prove that your business rules are always respected.
 - Run these checks in your CI/CD pipeline to ensure that no bug is introduced in your codebase.
 
-This adds a final layer of security to traditional code audits which are based on human reasoning and testing which only checks a finite amount of cases.
+This adds a final layer of security to traditional code audits which are based on human reasoning and testing which only checks a finite amount of cases. This verification even goes beyond other formal verification methods.
+
+![Verification process](./verification-techniques.png)
+_Picture from a [presentation](https://mikedodds.github.io/files/talks/2024-10-09-n-things-I-learned.pdf) of [Galois](https://galois.com/)_
 
 ## Typical workflow
 
 Formal verification is expensive ⏲️, so you should apply it after every other verification (testing, code review, etc.) is done. Here is a typical workflow:
 
 1. You model your smart contract in the Coq proof system. For this step, you manually rewrite your smart contract in idiomatic Coq code.
-2. You start expressing and proving a few properties in Coq about your model. For example, that for any possible call the total number of tokens in your contract is constant, if that is a business rule.
+2. You start expressing and proving a few properties in Coq about your model. For example, for any possible call the total number of tokens in your contract is constant, if that is a business rule.
 3. Once you are confident in the approach, you show that your model is equivalent to the Solidity source code using `coq-of-solidity` and integrate this check into your CI/CD pipeline. At this step, you will probably discover some differences between your model and the source code, like unaccounted integer overflows, and you will have to refine your model to take them into account.
 4. When your code evolves, you can update your model and your proofs to ensure that your new code is still correct. `coq-of-solidity` will make sure that your model is still equivalent to your source code 🚀.
 
@@ -96,7 +99,7 @@ Lemma run_checked_add_t_uint256 codes environment state
 
 It says that for any initial chain `state` and `x` and `y` such that they are in the range of `uint256`, if the addition does not overflow, then the result of the translation is the sum of `x` and `y`, and the chain `state` is unchanged. We could make a similar statement for the overflow case.
 
-Now we need to prove that this statement is true using the tactic language of Coq and some of the custom tactics provided by `coq-of-solidity`. We write the proof using the interactive mode of Coq. To give an idea, here is our proof:
+Now, we need to prove that this statement is true using the tactic language of Coq and some of the custom tactics provided by `coq-of-solidity`. We write the proof using the interactive mode of Coq. To give an idea, here is our proof:
 
 ```coq
 Proof.
@@ -129,3 +132,5 @@ We recommend only translating the unoptimized version of Yul. That way you are s
 
 - Keep the same variable names in the Coq translation as in the source Solidity, helping for the proof process.
 - Have a diff in the translation that is proportional to the diff in the source code.
+
+The implementation of `coq-of-solidity` is actually fairly simple and relies on the existing Coq system for the heavy work! 🏋️

coq/docs/src/presentation.md

@@ -0,0 +1,29 @@
+# Presentation
+
+Here is a 🏎️ quick presentation, in simple words, of what `coq-of-solidity` does.
+
+> With `coq-of-solidity` you make sure that the money stored on your Solidity smart contract cannot be stolen. 🛡️
+
+Every month, millions of dollars 💰 are stolen from smart contracts. This is because a single mistake in the code, even if this is just one line, lets an attacker withdraw all the money and disappear with it!
+
+Audits are mandatory, but this is a human 🧠 verifying the code, and mistakes are made.
+
+> 🚨 Even if major smart contracts have all been audited, they are still regularly hacked.
+
+With `coq-of-solidity`, the computer checks that the reasoning of the auditor is correct: this is like a spell checker for auditors.
+
+As a result, you can truly be sure that no attack scenario has been forgotten and that your smart contract is truly secure ✅.
+
+In addition, when you update the code of your smart contract, you can replay the reasoning for free to make sure your smart contract is still secure on the old part 😎 . This _saves on auditing costs_.
+
+## Why us?
+
+Verifying reasoning about code is called 🔎 _formal verification_. This is a complex technique 🧪 and very few companies have developed a tool to do this for Solidity. In addition, `coq-of-solidity` is the only one with [Clear](https://github.com/NethermindEth/Clear) that can express any possible reasoning/property on your code. This is thanks to the use of an 🐓 interactive theorem prover on the backend.
+
+At [🌲 Formal Land](https://formal.land/), where we developed `coq-of-solidity`, we are one of the leading teams applying formal verification to large-scale programs. We have developed two other formal verification tools, with [coq-of-rust](https://github.com/formal-land/coq-of-rust) for 🦀 Rust and [coq-of-ocaml](https://github.com/formal-land/coq-of-ocaml) for 🐫 OCaml. Read more about what we do on our [📖 blog](https://formal.land/blog).
+
+## How much? 💸
+
+For a large smart contract (5,000 lines of Solidity), consider a price of **$50,000** for a formal verification of a _model_ of the code, and **$100,000** for a verification at the level of the _source code_ (more precise). So, this is competitive with traditional audits.
+
+[💌 Contact us](mailto:contact@formal.land) for an evaluation!