Quando se trata de infraestrutura DeFi para instituições financeiras, segurança é requisito obrigatório e o próprio alicerce do produto. Foi com esse princípio que submetemos a suíte de smart contracts core da Levery à auditoria de segurança conduzida pela Runtime Verification, empresa sediada em Chicago, EUA, referência mundial em verificação formal e auditorias de código, confiada por protocolos líderes como Ethereum, Uniswap, EigenLayer, Lido, Maker e Optimism. O engajamento percorreu aproximadamente quatro semanas e meia e combinou revisão de design, inspeção manual minuciosa linha a linha em Solidity e técnicas de execução simbólica para validar propriedades de segurança sob uma ampla gama de cenários. O relatório final foi publicado em outubro de 2025.
A Levery permite que instituições financeiras e prestadores de serviços de ativos virtuais lancem suas próprias plataformas DeFi em conformidade com a regulação, cumprindo requisitos de KYC (Know Your Customer), KYB (Know Your Business) e AML (Anti-Money Laundering), com auto custódia e gestão dinâmica de taxas. Ao operar em ambientes regulados, precisamos demonstrar além de aderência técnica e operacional, mas também resiliência criptográfica, controle de superfícies de risco e qualidade de código auditável. Na prática, isso implica codificar mecanismos de permissão e governança que não apenas “funcionem” em condições ideais, mas que se mantenham corretos frente a inputs externos imperfeitos, à variabilidade de taxas de pool e a fluxos operacionais complexos de criação, aumento e queima de posições. O objetivo central da auditoria, portanto, foi demonstrar, por evidência técnica, que nossas invariantes de segurança e de economia se sustentam quando submetidas a um método adversarial e a análises formais.
Metodologia
O trabalho de auditoria teve início com um design review estruturado, no qual a Runtime Verification mapeou fronteiras de confiança, papéis de atores (traders, LPs, operadores de compliance e administradores), e os fluxos de ciclo de vida do protocolo. A partir desse mapeamento, foram definidas invariantes explícitas: nenhuma operação sensível deve ocorrer sem autorização válida e elegibilidade regulatória; os parâmetros de taxa precisam permanecer dentro de limites que preservem a estabilidade de liquidez; dados de oráculo não podem ser consumidos quando obsoletos, inconsistentes entre si ou fora da política definida; tokens de posição com natureza soulbound não podem, direta ou indiretamente, mudar de titularidade. Essas propriedades são a espinha dorsal do ambiente permissionado que concilia segurança operacional com as garantias de não-custódia.
Concluída a etapa de design, os auditores avançaram para a inspeção manual em Solidity, rastreando transições de estado e modos de falha ao longo dos contratos. Essa leitura linha a linha enfatizou ordem de checagens, mensagens de erro semânticas, tratamento de dependências externas e a ausência de rotas laterais que possam contornar os gates de conformidade.
Em paralelo, a RV executou métodos formais com execução simbólica para explorar, de forma sistemática, caminhos de execução que dificilmente emergem em testes convencionais. Nessa camada, a prioridade recaiu sobre saturações aritméticas (inclusive em espaços Q96/Q128), limites de parâmetros de taxa e efeitos de arredondamento, integridade e freshness de oráculos e o comportamento de controle de acesso sob diferentes permutações de papéis e eventos on-chain. Também foi uma oportunidade para “forçar” cenários de token mismatch em fluxos Permit2 e validar que domínios EIP-712, chainIds, pares de tokens e nonces são verificados de forma estrita antes de qualquer efeito sobre o estado.
Todos os achados identificados foram remediados em colaboração direta e contínua com os auditores, com documentação aprimorada e práticas operacionais claras. O código passou por hardening onde necessário; a suíte de testes foi ampliada para incluir casos-limite que reproduzem os cenários explorados pela execução simbólica; e a documentação operacional foi expandida para incorporar políticas de oráculo, playbooks de falha e telemetria sobre eventos críticos. O resultado prático é uma camada adicional de previsibilidade para quem precisa comprovar, perante comitês de risco e áreas de compliance, que a plataforma não depende de “boas condições” para funcionar corretamente. Em vez disso, ela codifica o que é admissível e torna verificável, por leitura, por teste e por prova, o que é vedado.
Por que este relatório de auditoria é relevante para instituições
Para instituições financeiras, isso se traduz em três efeitos tangíveis. Primeiro, conformidade por design: os gates de KYC/KYB/AML e os papéis com acesso restrito não são adendos processuais, mas pré-condições de execução em nível de contrato, preservando a natureza de auto custódia ao mesmo tempo em que reduzem o risco de contraparte comum em CEXs. Segundo, integridade de preço: ao atrelar o cálculo de taxas dinâmicas a sinais de oráculo com políticas de freshness e redundância, reduz-se a exposição a manipulações ou leituras obsoletas, um ponto sensível quando a precificação informa a própria economia do pool. Terceiro, auditabilidade operacional: regras de acesso, políticas de taxa e dependências externas são versionadas e observáveis, facilitando due diligence, integração com sistemas internos e o atendimento a obrigações regulatórias.
Além disso, a metodologia aplicada pela Runtime Verification cria uma base sólida para auditorias contínuas. O código foi estruturado de forma a facilitar revisões futuras, garantindo que alterações materiais passem por validação formal antes de serem adotadas em produção. Esse processo reduz riscos de regressão, facilita integração com sistemas institucionais e reforça a confiança no longo prazo.
Agradecimentos
Agradecemos à equipe da Runtime Verification pela profundidade técnica e colaboração, à Uniswap Foundation pelo apoio por meio do Security Fund e à Areta pela orquestração do processo.
Leia o relatório
A missão da Levery é conectar instituições à liquidez do DeFi preservando as garantias de segurança, controle e conformidade que o setor exige. Com o fechamento desta auditoria, reforçamos que o caminho passa por código legível, propriedades explícitas e validação independente. Para quem busca mais detalhes, o Relatório de Auditoria da Runtime Verification para a Levery está disponível para consulta e serve como referência técnica do estado atual dos contratos e das salvaguardas implementadas:
Detalhes do Relatório: https://amp.runtimeverification.com/public-report/levery
Download PDF
