EthSystems가 프라이버시 풀 형식 검증을 완료했으며, 규범을 Sepolia 바이트코드에 적용했습니다

이더리움 기관 프라이버시 기술 기관 EthSystems는 프라이버시 풀(차단 풀)에 대한 형식적 검증을 완료했다고 발표했습니다. 검증 범위는 서면 규격에서부터 Sepolia 테스트넷에서 실행되는 바이트코드까지 포함됩니다. 검증은 계층별로 다양한 도구를 사용하여 수행되었습니다: 모델, 회로 및 해시는 Lean을 사용하고, 계약은 Halmos와 Kontrol을, 지갑은 Aeneas와 Verus를 사용하며, 검증기와 배포는 바이트 단위로 재구성하여 확인합니다.

이중 지불 및 가치 보존은 Lean 정리 기계에 의해 검증되었습니다. 검증 중에 총 6개의 문제가 발견되었으며, 그 중 3개는 검증 도구 자체에서 발생했습니다. 팀은 여전히 의존하는 가정도 나열했습니다: 해시는 충돌이 없고, 검증기는 위조 증명을 거부하며, 계약 행동은 모델과 일치합니다.