fix spelling and formatting

program-analysis/manticore/exercises/example.md

@@ -1,23 +1,23 @@
 # Example: Arithmetic overflow
 This scenario is given as an example. You can follow its structure to solve the exercises.
 
-[`my_token.py`](example/my_token.py) uses manticore to find for an attacker to generate tokens during a transfer on Token ([my_token.sol](example/my_token.sol)).
+[`my_token.py`](example/my_token.py) uses Manticore to find for an attacker to generate tokens during a transfer on Token ([my_token.sol](example/my_token.sol)).
 
-## Proposed scenario
+## Proposed scenario
 
-We use the pattern initilization, exploration and property for our scripts.
+We use the pattern initialization, exploration and property for our scripts.
 
-### Initialization
+## Initialization
 
 - Create one user account
 - Create the contract account
 
-### Exploration
+## Exploration
 
 - Call balances on the user account
 - Call transfer with symbolic destination and value
 - Call balances on the user account
 
-### Property
+## Property
 
 - Check if the user can have more token after the transfer than before.

program-analysis/manticore/exercises/exercise1.md

@@ -1,32 +1,32 @@
 
-# Exercice 1 : Arithmetic
+# Exercise 1 : Arithmetic rounding
 
 Use Manticore to find an input allowing an attacker to generate free tokens in [exercise1/token.sol](./exercise1/token.sol).
 Propose a fix of the contract, and test your fix using your Manticore script.
 
 ## Proposed scenario
 
-Follow the pattern initilization, exploration and property for the script.
+Follow the pattern initialization, exploration and property for the script.
 
-### Initialization
+## Initialization
 
 - Create one account
 - Create the contract account
 
-### Exploration
+## Exploration
 
 - Call `is_valid_buy` with two symbolic values for tokens_amount and wei_amount
 
-### Property
+## Property
 
 - An attack is found if on a state alive `wei_amount == 0 and tokens_amount >= 1`
 
-### Hints
+## Hints
 
 - `m.ready_states` returns the list of state alive
 - `Operators.AND(a, b)` allows to create and AND condition
 - You can use the template proposed in [exercise1/template.py](./exercise1/template.py)
 
-### Solution
+## Solution
 
 [exercise1/solution.py](./exercise1/solution.py)

program-analysis/manticore/exercises/exercise2.md

@@ -1,12 +1,12 @@
-# Exercice 2 : Arithmetic on multi transactions
+# Exercise 2 : Arithmetic overflow through multiple transactions
 
 Use Manticore to find if an overflow is possible in Overflow.add. Propose a fix of the contract, and test your fix using your Manticore script.
 
 ## Proposed scenario
 
-Follow the pattern initilization, exploration and property for the script.
+Follow the pattern initialization, exploration and property for the script.
 
-### Initialization
+## Initialization
 
 - Create one user account
 - Create the contract account
@@ -20,7 +20,7 @@ Follow the pattern initilization, exploration and property for the script.
 
 - Check if it is possible for the value returned by sellerBalance() to be lower than the first input.
 
-## Hints:
+## Hints
 
 - The value returned by the last transaction can be accessed through:
 
@@ -36,6 +36,6 @@ data = ABI.deserialize("uint", data)
 
 - You can use the template proposed in [exercise2/template.py](./exercise2/template.py)
 
-### Solution
+## Solution
 
 [exercise2/solution.py](./exercise2/solution.py).