A Common Prefix está formalmente verificando o Protocolo de Empréstimo do $XRP Ledger para provar matematicamente que ele não pode ser esvaziado, tornar-se insolvente ou violar suas regras. O trabalho concentra-se no Protocolo de Empréstimo introduzido por meio do XLS-66. A Common Prefix explicou sua abordagem em uma série de seis partes, incluindo por que escolheu o Lean 4 para o processo de verificação. A Common Prefix afirmou que a verificação formal vai além dos testes de software normais, utilizando matemática para provar que um sistema funciona corretamente em todas as situações possíveis. O validador do XRP Ledger Vet, também conhecido como Hussein Zangana, disse que a verificação formal já é utilizada em sistemas de alto risco, como tecnologia militar, software de tráfego aéreo, controles de voo e usinas nucleares. Ele explicou que a abordagem usa matemática para demonstrar que um sistema permanece válido em todos os possíveis inputs, e não apenas nas situações testadas pelos desenvolvedores. A Common Prefix considerou várias ferramentas, incluindo Dafny, Lean 4, TLA+ e P. A equipe decidiu que TLA+ e P não eram adequados para as perguntas específicas que precisavam responder sobre o protocolo de empréstimo. Uma das razões para escolher o Lean 4 foi que ele não depende de um solucionador SMT. A Common Prefix descobriu que o solucionador do Dafny às vezes podia exceder o tempo limite ao lidar com a aritmética complexa necessária para a verificação. O Lean exige mais trabalho manual, mas isso também torna mais fácil para os desenvolvedores encontrar e corrigir erros. #Ripple https://t.co/s0YcQ4KAWX