Omfattende formell verifisering av @CetusProtocol på @SuiNetwork: kjerne CLMM-protokoll, standardbibliotek (STL) og heltallsmat. Vår formelle verifisering bekrefter korrektheten av kritiske protokollegenskaper, inkludert deduktive bevis for at tick-til-pris-konverteringsfunksjonene korrekt implementerer de matematiske formlene (√1.0001^tick og dens invers). Dette går langt utover alt annet formelt verifiseringsarbeid på Uniswap v3-lignende CLMM-protokoller, inkludert Uniswap selv. Som en del av vårt sikkerhetspartnerskap med Cetus vil vi fortsette å styrke protokollen deres. Detaljer og rapport nedenfor.