Scoping document can be found in the auditing repository.
MoMs of the sync meetings are found in the folder: SyncMoMs
TWAP module
GAMM module & Balancer style pools
- GAMM module spec improvements #3654
- Gamm code improvements #3657
- x/gamm module minor code improvements #3704
- Gamm balancer improvements #3836
GAMM module & Stableswap style pools
- Gamm stableswap improvements #3839
- TLA spec is created for balancer pool model type and it is modeling CreatePool, JoinPool, ExitPool and SwapExactAmountOut and SwapExactAmountIn transactions.
- Specification is located under models folder in osmosis-atomkraft submodule pointing to OsmosisAtomkraft version used during auditing of GAMM module.
- Osmosis atomkraft is adapted Informal Systems' in house build tool used during audits to help auditors find issues with generating and executing large number of apalache traces that could be executed on running chain. For more details check out our atomkraft repository and documentation.
Issues reported on Osmosis Lab github repositories:
-
ValidateFutureGovernor() needs some polishing #3664
-
JoinPoolNoSwap contains diff in calculation of the expected shares out and calculated shares out #3705
-
GAMM module and pool models' spec improvements #3706
-
x/gamm: define gas fee for stableswap pool swap computations #3837
-
GAMM: Suggestions for improving code structure #3841
-
x/gamm unit test coverage could be improved #3849
-
Atomkraft findings:
- x/gamm: Exiting balancer pool with zero assets and low share #3828
- x/gamm: Panics in SwapExactAmountOut and SwapExactAmountIn for balancer pool#3829
- x/gamm: Panic “division by zero” in SwapExactAmountOut for balancer pool #3831
- x/gamm: Unexpected error in MaximalExactRatioJoin for balancer JoinPoolNoSwap #3834