diff --git a/.circleci/config.yml b/.circleci/config.yml
index 9b521e62..28ec01f7 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -88,7 +88,7 @@ jobs:
           command: truffle compile
       - run:
           name: Slither
-          command: slither . --filter-paths test --exclude=naming-convention,unused-state,solc-version
+          command: slither . --filter-paths test --exclude=naming-convention,unused-state,solc-version,constable-states,external-function,reentrancy-events
 
 workflows:
   version: 2
diff --git a/.gitignore b/.gitignore
index fa1c825b..e8f2d013 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,4 +4,5 @@ node_modules
 coverage.json
 coverage/
 yarn-error.log
-crytic-export
\ No newline at end of file
+crytic-export
+mcore_*
\ No newline at end of file
diff --git a/.solcover.js b/.solcover.js
index bd07c7e3..5e08b372 100644
--- a/.solcover.js
+++ b/.solcover.js
@@ -1,9 +1,8 @@
 module.exports = {
   port: 8555,
   skipFiles: [
-    'BStub.sol',
     'Migrations.sol',
     'test'
   ],
-  testrpcOptions: "-p 8555 -d --allowUnlimitedContractSize"
+  testrpcOptions: "-p 8555 -d"
 };
\ No newline at end of file
diff --git a/Audit.md b/Audit.md
index 88ac8a01..b3239b49 100644
--- a/Audit.md
+++ b/Audit.md
@@ -46,14 +46,14 @@ To test a property, run `echidna-test echidna/CONTRACT_file.sol CONTRACT_name --
 
 ## General Properties
 
-| Description    | Name           | Contract      | Status   |  
-| :---                                                            |     :---:              |         :---:   |  :---:   |
-| An attacker cannot steal assets from a public pool.              | [`attacker_token_balance`](echidna/TBPoolBalance.sol#L22-L25)   | [`TBPoolBalance`](echidna/TBPoolBalance.sol) |**FAILED** ([#193](https://github.com/balancer-labs/balancer-core/issues/193))|
-| An attacker cannot force the pool balance to be out-of-sync.  | [`pool_record_balance`](echidna/TBPoolBalance.sol#L27-L33)  | [`TBPoolBalance`](echidna/TBPoolBalance.sol)|**PASSED**|
-| An attacker cannot generate free pool tokens with `joinPool` (1, 2).  | [`joinPool`](contracts/test/echidna/TBPoolJoinPool.sol#L7-L31)  | [`TBPoolJoinPool`](contracts/test/echidna/TBPoolBalance.sol)|**FAILED** ([#204](https://github.com/balancer-labs/balancer-core/issues/204))|
-| Calling `joinPool-exitPool` does not lead to free pool tokens (no fee) (1, 2).  | [`joinPool`](contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol#L34-L59)  | [`TBPoolJoinExitNoFee`](contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol)|**FAILED** ([#205](https://github.com/balancer-labs/balancer-core/issues/205))|
-| Calling `joinPool-exitPool` does not lead to free pool tokens (with fee) (1, 2).  | [`joinPool`](contracts/test/echidna/TBPoolJoinExitPool.sol#L37-L62)  | [`TBPoolJoinExit`](contracts/test/echidna/TBPoolJoinExitPool.sol)|**FAILED** ([#205](https://github.com/balancer-labs/balancer-core/issues/205))|
-| Calling `exitswapExternAmountOut` does not lead to free asset (1).  | [`exitswapExternAmountOut`](echidna/TBPoolExitSwap.sol#L8-L21)  | [`TBPoolExitSwap`](contracts/test/echidna/TBPoolExitSwap.sol)|**FAILED** ([#203](https://github.com/balancer-labs/balancer-core/issues/203))|
+| Description    | Name           | Contract      | Finding   | Status   | 
+| :---                                                            |     :---:              |         :---:   |  :---:   | :---:   |
+| An attacker cannot steal assets from a public pool.              | [`attacker_token_balance`](echidna/TBPoolBalance.sol#L22-L25)   | [`TBPoolBalance`](echidna/TBPoolBalance.sol) |FAILED ([#193](https://github.com/balancer-labs/balancer-core/issues/193))| **Fixed** |
+| An attacker cannot force the pool balance to be out-of-sync.  | [`pool_record_balance`](echidna/TBPoolBalance.sol#L27-L33)  | [`TBPoolBalance`](echidna/TBPoolBalance.sol)|PASSED|  |
+| An attacker cannot generate free pool tokens with `joinPool` (1, 2).  | [`joinPool`](contracts/test/echidna/TBPoolJoinPool.sol#L7-L31)  | [`TBPoolJoinPool`](contracts/test/echidna/TBPoolBalance.sol)|FAILED ([#204](https://github.com/balancer-labs/balancer-core/issues/204))|  **Mitigated** |
+| Calling `joinPool-exitPool` does not lead to free pool tokens (no fee) (1, 2).  | [`joinPool`](contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol#L34-L59)  | [`TBPoolJoinExitNoFee`](contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol)|FAILED ([#205](https://github.com/balancer-labs/balancer-core/issues/205))| **Mitigated** |
+| Calling `joinPool-exitPool` does not lead to free pool tokens (with fee) (1, 2).  | [`joinPool`](contracts/test/echidna/TBPoolJoinExitPool.sol#L37-L62)  | [`TBPoolJoinExit`](contracts/test/echidna/TBPoolJoinExitPool.sol)|FAILED ([#205](https://github.com/balancer-labs/balancer-core/issues/205))| **Mitigated** |
+| Calling `exitswapExternAmountOut` does not lead to free asset (1).  | [`exitswapExternAmountOut`](echidna/TBPoolExitSwap.sol#L8-L21)  | [`TBPoolExitSwap`](contracts/test/echidna/TBPoolExitSwap.sol)|FAILED ([#203](https://github.com/balancer-labs/balancer-core/issues/203))| **Mitigated** |
 
 
 (1) These properties target a specific piece of code.
@@ -62,42 +62,41 @@ To test a property, run `echidna-test echidna/CONTRACT_file.sol CONTRACT_name --
 
 ## Unit-test-based Properties
 
-| Description    | Name           | Contract      | Status   |  
-| :---                                                            |     :---:              |         :---:   |  :---:   |
-| If the controller calls `setController`, then the `getController()` should return the new controller.  | [`controller_should_change`](echidna/TBPoolController.sol#L6-L13)  | [`TBPoolController`](echidna/TBPoolController.sol)|**PASSED**|
-| The controller cannot be changed to a null address (`0x0`).  | [`controller_cannot_be_null`](echidna/TBPoolController.sol#L15-L23)  | [`TBPoolController`](echidna/TBPoolController.sol)|**FAILED** ([#198](https://github.com/balancer-labs/balancer-core/issues/198))|
-| The controller cannot be changed by other users.  | [`no_other_user_can_change_the_controller`](echidna/TBPoolController.sol#L28-L31)  | [`TBPoolController`](echidna/TBPoolController.sol)|**PASSED**|
-| The sum of normalized weight should be 1 if there are tokens binded.  | [`valid_weights`](echidna/TBPoolLimits.sol#L35-L52)  | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |**FAILED** ([#208](https://github.com/balancer-labs/balancer-core/issues/208)|
-| The balances of all the tokens are less or equal than `MAX_BALANCE`.  | [`max_token_balance`](echidna/TBPoolLimits.sol#L54-L63)  | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |**FAILED** ([#210](https://github.com/balancer-labs/balancer-core/issues/210))|
-| The balances of all the tokens are greater or equal than `MIN_BALANCE`.  | [`min_token_balance`](echidna/TBPoolLimits.sol#L65-L74)  | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |**FAILED** ([#210](https://github.com/balancer-labs/balancer-core/issues/210)) |
-| The weight of all the tokens are less or equal than `MAX_WEIGHT`.  | [`max_weight`](echidna/TBPoolLimits.sol#L76-L85)  | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |**PASSED**|
-| The weight of all the tokens are greater or equal than `MIN_WEIGHT`.  | [`min_weight`](echidna/TBPoolLimits.sol#L87-L96)  | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |**PASSED**|
-| The swap fee is less or equal tan `MAX_FEE`. | [`min_swap_free`](echidna/TBPoolLimits.sol#L99-L102)  | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |**PASSED**|
-| The swap fee is greater or equal than `MIN_FEE`.  | [`max_swap_free`](echidna/TBPoolLimits.sol#L104-L107)  | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |**PASSED**|
-| An user can only swap in less than 50% of the current balance of tokenIn for a given pool. | [`max_swapExactAmountIn`](echidna/TBPoolLimits.sol#L134-L156) | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |**FAILED** ([#212](https://github.com/balancer-labs/balancer-core/issues/212))|
-| An user can only swap out less than 33.33% of the current balance of tokenOut for a given pool. | [`max_swapExactAmountOut`](echidna/TBPoolLimits.sol#L109-L132) | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |**FAILED** ([#212](https://github.com/balancer-labs/balancer-core/issues/212))|
-| If a token is bounded, the `getSpotPrice` should never revert.  | [`getSpotPrice_no_revert`](echidna/TBPoolNoRevert.sol#L34-L44)  | [`TBPoolNoRevert`](echidna/TBPoolNoRevert.sol) |**PASSED**|
-| If a token is bounded, the `getSpotPriceSansFee` should never revert.  | [`getSpotPriceSansFee_no_revert`](echidna/TBPoolNoRevert.sol#L46-L56)  | [`TBPoolNoRevert`](echidna/TBPoolNoRevert.sol) |**PASSED**|
-| Calling `swapExactAmountIn` with a small value of the same token should never revert.  | [`swapExactAmountIn_no_revert`](echidna/TBPoolNoRevert.sol#L58-L77)  | [`TBPoolNoRevert`](echidna/TBPoolNoRevert.sol) |**PASSED**|
-| Calling `swapExactAmountOut` with a small value of the same token should never revert. | [`swapExactAmountOut_no_revert`](echidna/TBPoolNoRevert.sol#L79-L99)  | [`TBPoolNoRevert`](echidna/TBPoolNoRevert.sol) |**PASSED**|
-| If a user joins pool and exits it with the same amount, the balances should keep constant.  | [`joinPool_exitPool_balance_consistency`](echidna/TBPoolJoinExit.sol#L48-L97)  | [`TBPoolJoinExit`](echidna/TBPoolJoinExit.sol) |**PASSED**|
-| If a user joins pool and exits it with a larger amount, `exitPool` should revert.  | [`impossible_joinPool_exitPool`](echidna/TBPoolJoinExit.sol#L99-L112) | [`TBPoolJoinExit`](echidna/TBPoolJoinExit.sol) |**PASSED**|
-| It is not possible to bind more than `MAX_BOUND_TOKENS`. | [`getNumTokens_less_or_equal_MAX_BOUND_TOKENS`](echidna/TBPoolBind.sol#L40-L43)  | [`TBPoolBind`](echidna/TBPoolBind.sol) |**PASSED**|
-| It is not possible to bind more than once the same token.  | [`bind_twice`](echidna/TBPoolBind.sol#L45-L54)  | [`TBPoolBind`](echidna/TBPoolBind.sol) |**PASSED**|
-| It is not possible to unbind more than once the same token. | [`unbind_twice`](echidna/TBPoolBind.sol#L56-L66)  | [`TBPoolBind`](echidna/TBPoolBind.sol) |**PASSED**|
-| It is always possible to unbind a token.  | [`all_tokens_are_unbindable`](echidna/TBPoolBind.sol#L68-L81)  | [`TBPoolBind`](echidna/TBPoolBind.sol) |**PASSED**|
-| All tokens are rebindable with valid parameters. | [`all_tokens_are_rebindable_with_valid_parameters`](echidna/TBPoolBind.sol#L83-L95)  | [`TBPoolBind`](echidna/TBPoolBind.sol) |**PASSED**|
-| It is not possible to rebind an unbinded token. | [`rebind_unbinded`](echidna/TBPoolBind.sol#L97-L107)  | [`TBPoolBind`](echidna/TBPoolBind.sol) |**PASSED**|
-| Only the controller can bind. | [`when_bind`](echidna/TBPoolBind.sol#L150-L154) and [`only_controller_can_bind`](echidna/TBPoolBind.sol#L145-L148) | [`TBPoolBind`](echidna/TBPoolBind.sol) |**PASSED**|
-| If a user that is not the controller, tries to bind, rebind or unbind, the operation will revert. | [`when_bind`](echidna/TBPoolBind.sol#L150-L154), [`when_rebind`](echidna/TBPoolBind.sol#L150-L154) and [`when_unbind`](echidna/TBPoolBind.sol#L163-L168)  | [`TBPoolBind`](echidna/TBPoolBind.sol) |**PASSED**|
-| Transfer tokens to the null address (`0x0`) causes a revert | [`transfer_to_zero`](echidna/TBTokenERC20.sol#L75-L79) and [`transferFrom_to_zero`](echidna/TBTokenERC20.sol#L85-L89) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |**FAILED** ([#197](https://github.com/balancer-labs/balancer-core/issues/197))|
-| The null address (`0x0`) owns no tokens | [`zero_always_empty`](echidna/TBTokenERC20.sol#L34-L36) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |**FAILED**|
-| Transfer a valid amout of tokens to non-null address reduces the current balance | [`transferFrom_to_other`](echidna/TBTokenERC20.sol#L108-L113) and [`transfer_to_other`](echidna/TBTokenERC20.sol#L131-L142)  | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |**PASSED**|
-| Transfer an invalid amout of tokens to non-null address reverts or returns false | [`transfer_to_user`](echidna/TBTokenERC20.sol#L149-L155) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |**PASSED**|
-| Self transfer a valid amout of tokens keeps the current balance constant | [`self_transferFrom`](echidna/TBTokenERC20.sol#L96-L101) and [`self_transfer`](echidna/TBTokenERC20.sol#L120-L124) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |**PASSED**|
-| Approving overwrites the previous allowance value | [`approve_overwrites`](echidna/TBTokenERC20.sol#L42-L49) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |**PASSED**|
-| The `totalSupply` is a constant | [`totalSupply_constant`](echidna/TBTokenERC20.sol#L166-L168) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |**PASSED**|
-| The balances are consistent with the `totalSupply` | [`totalSupply_balances_consistency`](echidna/TBTokenERC20.sol#L63-L65) and [`balance_less_than_totalSupply`](echidna/TBTokenERC20.sol#L55-L57) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |**PASSED**|
+| Description    | Name           | Contract      | Finding   |  Status   |
+| :---                                                            |     :---:              |         :---:   |  :---:   |  :---:   |
+| If the controller calls `setController`, then the `getController()` should return the new controller.  | [`controller_should_change`](echidna/TBPoolController.sol#L6-L13)  | [`TBPoolController`](echidna/TBPoolController.sol)|PASSED| |
+| The controller cannot be changed to a null address (`0x0`).  | [`controller_cannot_be_null`](echidna/TBPoolController.sol#L15-L23)  | [`TBPoolController`](echidna/TBPoolController.sol)|FAILED ([#198](https://github.com/balancer-labs/balancer-core/issues/198))| **WONT FIX** |
+| The controller cannot be changed by other users.  | [`no_other_user_can_change_the_controller`](echidna/TBPoolController.sol#L28-L31)  | [`TBPoolController`](echidna/TBPoolController.sol)|PASSED| |
+| The sum of normalized weight should be 1 if there are tokens binded.  | [`valid_weights`](echidna/TBPoolLimits.sol#L35-L52)  | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |FAILED ([#208](https://github.com/balancer-labs/balancer-core/issues/208)| **Mitigated** |
+| The balances of all the tokens are greater or equal than `MIN_BALANCE`.  | [`min_token_balance`](echidna/TBPoolLimits.sol#L65-L74)  | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |FAILED ([#210](https://github.com/balancer-labs/balancer-core/issues/210)) | **WONT FIX**|
+| The weight of all the tokens are less or equal than `MAX_WEIGHT`.  | [`max_weight`](echidna/TBPoolLimits.sol#L76-L85)  | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |PASSED| |
+| The weight of all the tokens are greater or equal than `MIN_WEIGHT`.  | [`min_weight`](echidna/TBPoolLimits.sol#L87-L96)  | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |PASSED| |
+| The swap fee is less or equal tan `MAX_FEE`. | [`min_swap_free`](echidna/TBPoolLimits.sol#L99-L102)  | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |PASSED| |
+| The swap fee is greater or equal than `MIN_FEE`.  | [`max_swap_free`](echidna/TBPoolLimits.sol#L104-L107)  | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |PASSED| |
+| An user can only swap in less than 50% of the current balance of tokenIn for a given pool. | [`max_swapExactAmountIn`](echidna/TBPoolLimits.sol#L134-L156) | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |FAILED ([#212](https://github.com/balancer-labs/balancer-core/issues/212))| **Fixed** |
+| An user can only swap out less than 33.33% of the current balance of tokenOut for a given pool. | [`max_swapExactAmountOut`](echidna/TBPoolLimits.sol#L109-L132) | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |FAILED ([#212](https://github.com/balancer-labs/balancer-core/issues/212))|  **Fixed** |
+| If a token is bounded, the `getSpotPrice` should never revert.  | [`getSpotPrice_no_revert`](echidna/TBPoolNoRevert.sol#L34-L44)  | [`TBPoolNoRevert`](echidna/TBPoolNoRevert.sol) |PASSED| |
+| If a token is bounded, the `getSpotPriceSansFee` should never revert.  | [`getSpotPriceSansFee_no_revert`](echidna/TBPoolNoRevert.sol#L46-L56)  | [`TBPoolNoRevert`](echidna/TBPoolNoRevert.sol) |PASSED| |
+| Calling `swapExactAmountIn` with a small value of the same token should never revert.  | [`swapExactAmountIn_no_revert`](echidna/TBPoolNoRevert.sol#L58-L77)  | [`TBPoolNoRevert`](echidna/TBPoolNoRevert.sol) |PASSED| |
+| Calling `swapExactAmountOut` with a small value of the same token should never revert. | [`swapExactAmountOut_no_revert`](echidna/TBPoolNoRevert.sol#L79-L99)  | [`TBPoolNoRevert`](echidna/TBPoolNoRevert.sol) |PASSED| |
+| If a user joins pool and exits it with the same amount, the balances should keep constant.  | [`joinPool_exitPool_balance_consistency`](echidna/TBPoolJoinExit.sol#L48-L97)  | [`TBPoolJoinExit`](echidna/TBPoolJoinExit.sol) |PASSED| |
+| If a user joins pool and exits it with a larger amount, `exitPool` should revert.  | [`impossible_joinPool_exitPool`](echidna/TBPoolJoinExit.sol#L99-L112) | [`TBPoolJoinExit`](echidna/TBPoolJoinExit.sol) |PASSED| |
+| It is not possible to bind more than `MAX_BOUND_TOKENS`. | [`getNumTokens_less_or_equal_MAX_BOUND_TOKENS`](echidna/TBPoolBind.sol#L40-L43)  | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| |
+| It is not possible to bind more than once the same token.  | [`bind_twice`](echidna/TBPoolBind.sol#L45-L54)  | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| |
+| It is not possible to unbind more than once the same token. | [`unbind_twice`](echidna/TBPoolBind.sol#L56-L66)  | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| |
+| It is always possible to unbind a token.  | [`all_tokens_are_unbindable`](echidna/TBPoolBind.sol#L68-L81)  | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| |
+| All tokens are rebindable with valid parameters. | [`all_tokens_are_rebindable_with_valid_parameters`](echidna/TBPoolBind.sol#L83-L95)  | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| |
+| It is not possible to rebind an unbinded token. | [`rebind_unbinded`](echidna/TBPoolBind.sol#L97-L107)  | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| |
+| Only the controller can bind. | [`when_bind`](echidna/TBPoolBind.sol#L150-L154) and [`only_controller_can_bind`](echidna/TBPoolBind.sol#L145-L148) | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| |
+| If a user that is not the controller, tries to bind, rebind or unbind, the operation will revert. | [`when_bind`](echidna/TBPoolBind.sol#L150-L154), [`when_rebind`](echidna/TBPoolBind.sol#L150-L154) and [`when_unbind`](echidna/TBPoolBind.sol#L163-L168)  | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| |
+| Transfer tokens to the null address (`0x0`) causes a revert | [`transfer_to_zero`](echidna/TBTokenERC20.sol#L75-L79) and [`transferFrom_to_zero`](echidna/TBTokenERC20.sol#L85-L89) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |FAILED ([#197](https://github.com/balancer-labs/balancer-core/issues/197))| **WONT FIX** |
+| The null address (`0x0`) owns no tokens | [`zero_always_empty`](echidna/TBTokenERC20.sol#L34-L36) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |FAILED| **WONT FIX** |
+| Transfer a valid amout of tokens to non-null address reduces the current balance | [`transferFrom_to_other`](echidna/TBTokenERC20.sol#L108-L113) and [`transfer_to_other`](echidna/TBTokenERC20.sol#L131-L142)  | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |PASSED| |
+| Transfer an invalid amout of tokens to non-null address reverts or returns false | [`transfer_to_user`](echidna/TBTokenERC20.sol#L149-L155) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |PASSED| |
+| Self transfer a valid amout of tokens keeps the current balance constant | [`self_transferFrom`](echidna/TBTokenERC20.sol#L96-L101) and [`self_transfer`](echidna/TBTokenERC20.sol#L120-L124) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |PASSED| |
+| Approving overwrites the previous allowance value | [`approve_overwrites`](echidna/TBTokenERC20.sol#L42-L49) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |PASSED| |
+| The `totalSupply` is a constant | [`totalSupply_constant`](echidna/TBTokenERC20.sol#L166-L168) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |PASSED| |
+| The balances are consistent with the `totalSupply` | [`totalSupply_balances_consistency`](echidna/TBTokenERC20.sol#L63-L65) and [`balance_less_than_totalSupply`](echidna/TBTokenERC20.sol#L55-L57) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |PASSED| |
 
 # Code verification with Manticore
 
diff --git a/README.md b/README.md
index c52bfc8e..8583cf1b 100644
--- a/README.md
+++ b/README.md
@@ -24,7 +24,7 @@ your portfolio by following arbitrage opportunities.
 
 Balancer is based on an N-dimensional invariant surface which is a generalization of the constant product formula described by Vitalik Buterin and proven viable by the popular Uniswap dapp.
 
-<h2 align=center><br/><code>🍂 bronze release 🍂</code></h2>
+## 🍂 Bronze Release 🍂
 
 The *🍂Bronze Release🍂*  is the first of 3 planned releases of the Balancer Protocol. Bronze emphasizes code clarity for audit and verification, and does not go to great lengths to optimize for gas.
 
@@ -32,8 +32,12 @@ The *❄️Silver Release❄️* will bring many gas optimizations and architect
 
 The *☀️Golden Release☀️* will introduce a curious new liquidity mechanism to the market.
 
+## Documentation
 
-### Using the ABI definitions
+The full documentation can be found at [https://docs.balancer.finance](https://docs.balancer.finance)
+
+
+## Development
 
 Most users will want to consume the ABI definitions for BFactory and BPool.
 
@@ -73,8 +77,7 @@ relDif  : 1.6464292361378058e-12)
       ✓ exitswap_ExternAmountOut (537ms)
 ```
 
-Complete API docs are available at [https://balancer.finance/api](https://balancer.finance/api)
-(or see the [markdown source](https://github.com/balancer-labs/balancer-finance/blob/master/api.md) if it's not available).
-Look in the [`test/`](https://github.com/balancer-labs/balancer-core/tree/master/test) directory for working examples in a mock environment.
+Complete API docs are available at [https://docs.balancer.finance/smart-contracts/api](https://docs.balancer.finance/smart-contracts/api)
+
 
 <p align=center>⊙</p>
diff --git a/contracts/test/echidna/TBPoolJoinExitPool.sol b/contracts/test/echidna/TBPoolJoinExitPool.sol
index 1c5acd0d..625f122a 100644
--- a/contracts/test/echidna/TBPoolJoinExitPool.sol
+++ b/contracts/test/echidna/TBPoolJoinExitPool.sol
@@ -1,5 +1,7 @@
 import "../../BNum.sol";
 
+pragma solidity 0.5.12;
+
 //  This test is similar to TBPoolJoin but with an exit fee
 contract TBPoolJoinExit is BNum {
 
@@ -7,7 +9,7 @@ contract TBPoolJoinExit is BNum {
 
     // joinPool models the BPool.joinPool behavior for one token
     function joinPool(uint poolAmountOut, uint poolTotal, uint _records_t_balance)
-        internal returns(uint)
+        internal pure returns(uint)
     {
         uint ratio = bdiv(poolAmountOut, poolTotal);
         require(ratio != 0, "ERR_MATH_APPROX");
@@ -20,7 +22,7 @@ contract TBPoolJoinExit is BNum {
 
     // exitPool models the BPool.exitPool behavior for one token
     function exitPool(uint poolAmountIn, uint poolTotal, uint _records_t_balance)
-        internal returns(uint)
+        internal pure returns(uint)
     {
         uint exitFee = bmul(poolAmountIn, EXIT_FEE);
         uint pAiAfterExitFee = bsub(poolAmountIn, exitFee);
diff --git a/contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol b/contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol
index 85b4aa95..5b311147 100644
--- a/contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol
+++ b/contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol
@@ -1,5 +1,7 @@
 import "../../BNum.sol";
 
+pragma solidity 0.5.12;
+
 //  This test is similar to TBPoolJoinExit but with no exit fee
 contract TBPoolJoinExitNoFee is BNum {
 
@@ -7,7 +9,7 @@ contract TBPoolJoinExitNoFee is BNum {
 
     // joinPool models the BPool.joinPool behavior for one token
     function joinPool(uint poolAmountOut, uint poolTotal, uint _records_t_balance)
-        internal returns(uint)
+        internal pure returns(uint)
     {
         uint ratio = bdiv(poolAmountOut, poolTotal);
         require(ratio != 0, "ERR_MATH_APPROX");
@@ -20,7 +22,7 @@ contract TBPoolJoinExitNoFee is BNum {
 
     // exitPool models the BPool.exitPool behavior for one token where no fee is applied
     function exitPoolNoFee(uint poolAmountIn, uint poolTotal, uint _records_t_balance)
-        internal returns(uint)
+        internal pure returns(uint)
     {
         uint ratio = bdiv(poolAmountIn, poolTotal);
         require(ratio != 0, "ERR_MATH_APPROX");
@@ -33,7 +35,9 @@ contract TBPoolJoinExitNoFee is BNum {
 
     // This function model an attacker calling joinPool - exitPool and taking advantage of potential rounding
     // issues to generate free pool token
-    function joinAndExitNoFeePool(uint poolAmountOut, uint poolAmountIn, uint poolTotal, uint _records_t_balance) public {
+    function joinAndExitNoFeePool(uint poolAmountOut, uint poolAmountIn, uint poolTotal, uint _records_t_balance)
+        public 
+    {
         uint tokenAmountIn = joinPool(poolAmountOut, poolTotal, _records_t_balance);
 
         // We constraint poolTotal and _records_t_balance
diff --git a/contracts/test/echidna/TBPoolJoinPool.sol b/contracts/test/echidna/TBPoolJoinPool.sol
index 6ed3444d..d43ec43b 100644
--- a/contracts/test/echidna/TBPoolJoinPool.sol
+++ b/contracts/test/echidna/TBPoolJoinPool.sol
@@ -1,5 +1,7 @@
 import "../../BNum.sol";
 
+pragma solidity 0.5.12;
+
 contract TBPoolJoinPool is BNum {
 
     bool public echidna_no_bug_found = true;
diff --git a/echidna/TBPoolJoinExit.sol b/echidna/TBPoolJoinExit.sol
index 3012a7f1..a23c60b0 100644
--- a/echidna/TBPoolJoinExit.sol
+++ b/echidna/TBPoolJoinExit.sol
@@ -4,6 +4,8 @@ import "./CryticInterface.sol";
 
 contract TBPoolJoinExit is CryticInterface, BPool {
 
+    uint MAX_BALANCE = BONE * 10**12;
+
     constructor() public {
         MyToken t;
         t = new MyToken(uint(-1), address(this));
diff --git a/echidna/TBPoolLimits.sol b/echidna/TBPoolLimits.sol
index 85ba17d9..4493db7a 100644
--- a/echidna/TBPoolLimits.sol
+++ b/echidna/TBPoolLimits.sol
@@ -4,6 +4,8 @@ import "./CryticInterface.sol";
 
 contract TBPoolLimits is CryticInterface, BPool {
 
+    uint MAX_BALANCE = BONE * 10**12;
+
     constructor() public {
         MyToken t;
         t = new MyToken(uint(-1), address(this));
@@ -50,17 +52,6 @@ contract TBPoolLimits is CryticInterface, BPool {
         // if there are tokens, the normalized weight should be 1
         return (nw == 1);
     }
-    
-    function echidna_max_token_balance() public returns (bool) {
-         address[] memory current_tokens = this.getCurrentTokens();
-         for (uint i = 0; i < current_tokens.length; i++) {
-             // verify that the balance of each token is less than `MAX_BALACE`
-             if (this.getBalance(address(current_tokens[i])) > MAX_BALANCE)
-                 return false;
-         }
-         // if there are no tokens, return true
-         return true;
-    }
 
     function echidna_min_token_balance() public returns (bool) {
         address[] memory current_tokens = this.getCurrentTokens();
diff --git a/manticore/TBPoolJoinExitNoFee.py b/manticore/TBPoolJoinExitNoFee.py
index 16598a0b..4f049712 100644
--- a/manticore/TBPoolJoinExitNoFee.py
+++ b/manticore/TBPoolJoinExitNoFee.py
@@ -34,8 +34,8 @@ def will_evm_execute_instruction_callback(self, state, instruction, arguments):
 skipRequire = SkipRequire()
 m.register_plugin(skipRequire)
 
-TestBpool = m.solidity_create_contract('./manticore/contracts/TestJoinExitNoFee.sol',
-                                       contract_name='TestJoinExitNoFee',
+TestBpool = m.solidity_create_contract('./manticore/contracts/TBPoolJoinExitNoFee.sol',
+                                       contract_name='TBPoolJoinExitNoFee',
                                        owner=user)
 
 print(f'TestJoinExit deployed {hex(TestBpool.address)}')
diff --git a/manticore/TBPoolJoinPool.py b/manticore/TBPoolJoinPool.py
index 051d4484..09b16875 100644
--- a/manticore/TBPoolJoinPool.py
+++ b/manticore/TBPoolJoinPool.py
@@ -42,10 +42,9 @@ def will_evm_execute_instruction_callback(self, state, instruction, arguments):
 
 # Call joinAndExitNoFeePool with symbolic values
 poolAmountOut = m.make_symbolic_value()
-poolAmountIn = m.make_symbolic_value()
 poolTotal = m.make_symbolic_value()
 _records_t_balance = m.make_symbolic_value()
-TestBpool.joinPool(poolAmountOut, poolAmountIn, poolTotal, _records_t_balance)
+TestBpool.joinPool(poolAmountOut, poolTotal, _records_t_balance)
 
 print(f'joinPool Called')
 
diff --git a/manticore/contracts/BNum.sol b/manticore/contracts/BNum.sol
index be5910ad..e6708bd3 100644
--- a/manticore/contracts/BNum.sol
+++ b/manticore/contracts/BNum.sol
@@ -1,5 +1,3 @@
-pragma solidity 0.5.12;
-    
 // This file is a flatenen verison of BNum
 // where require(cond, string) where replaced by require(cond)
 // To allow SkipRequire to work properly
diff --git a/manticore/contracts/TBPoolJoinExitPool.sol b/manticore/contracts/TBPoolJoinExitPool.sol
index 9f9b092d..03487b51 100644
--- a/manticore/contracts/TBPoolJoinExitPool.sol
+++ b/manticore/contracts/TBPoolJoinExitPool.sol
@@ -5,7 +5,7 @@ contract TBPoolJoinExit is BNum {
 
     // joinPool models the BPool.joinPool behavior for one token
     function joinPool(uint poolAmountOut, uint poolTotal, uint _records_t_balance)
-        internal returns(uint)
+        internal pure returns(uint)
     {
         uint ratio = bdiv(poolAmountOut, poolTotal);
         require(ratio != 0);
@@ -18,7 +18,7 @@ contract TBPoolJoinExit is BNum {
 
     // exitPool models the BPool.exitPool behavior for one token
     function exitPool(uint poolAmountIn, uint poolTotal, uint _records_t_balance)
-        internal returns(uint)
+        internal pure returns(uint)
     {
         uint exitFee = bmul(poolAmountIn, EXIT_FEE);
         uint pAiAfterExitFee = bsub(poolAmountIn, exitFee);
@@ -34,7 +34,7 @@ contract TBPoolJoinExit is BNum {
 
     // This function model an attacker calling joinPool - exitPool and taking advantage of potential rounding
     // issues to generate free pool token
-    function joinAndExitPool(uint poolAmountOut, uint poolAmountIn, uint poolTotal, uint _records_t_balance) public {
+    function joinAndExitPool(uint poolAmountOut, uint poolAmountIn, uint poolTotal, uint _records_t_balance) public pure {
         uint tokenAmountIn = joinPool(poolAmountOut, poolTotal, _records_t_balance);
 
         // We constraint poolTotal and _records_t_balance
diff --git a/manticore/contracts/TBPoolJoinExitPoolNoFee.sol b/manticore/contracts/TBPoolJoinExitPoolNoFee.sol
index b443812d..703ca1d4 100644
--- a/manticore/contracts/TBPoolJoinExitPoolNoFee.sol
+++ b/manticore/contracts/TBPoolJoinExitPoolNoFee.sol
@@ -3,9 +3,11 @@ import "./BNum.sol";
 //  This test is similar to TBPoolJoinExit but with no exit fee
 contract TBPoolJoinExitNoFee is BNum {
 
+    bool public echidna_no_bug_found = true;
+
     // joinPool models the BPool.joinPool behavior for one token
     function joinPool(uint poolAmountOut, uint poolTotal, uint _records_t_balance)
-        internal returns(uint)
+        internal pure returns(uint)
     {
         uint ratio = bdiv(poolAmountOut, poolTotal);
         require(ratio != 0);
@@ -18,7 +20,7 @@ contract TBPoolJoinExitNoFee is BNum {
 
     // exitPool models the BPool.exitPool behavior for one token where no fee is applied
     function exitPoolNoFee(uint poolAmountIn, uint poolTotal, uint _records_t_balance)
-        internal returns(uint)
+        internal pure returns(uint)
     {
         uint ratio = bdiv(poolAmountIn, poolTotal);
         require(ratio != 0);