Verificação formal abrangente de @CetusProtocol em @SuiNetwork: protocolo CLMM central, biblioteca padrão (STL) e integer-mate. Nossa verificação formal confirma a correção das propriedades críticas do protocolo, incluindo provas dedutivas de que as funções de conversão de tick-para-preço implementam corretamente as fórmulas matemáticas (√1,0001^tick e seu inverso). Isso vai muito além de todo outro trabalho formal de verificação nos protocolos CLMM do estilo Uniswap v3, incluindo o próprio Uniswap. Como parte da nossa parceria de segurança com a Cetus, continuaremos reforçando o protocolo deles. Detalhes e relatório abaixo.