PANews 10월 27일 소식, 이더리움 기관 프라이버시 기술 기관 EthSystems가 자사의 프라이버시 풀(shielded pool)에 대한 형식 검증을 완료했다고 발표했다. 검증 범위는 문서화된 명세부터 Sepolia 테스트넷에서 실행되는 바이트코드까지다.
검증은 계층별로 서로 다른 도구를 사용했다. 모델·회로·해시는 Lean, 컨트랙트는 Halmos와 Kontrol, 지갑은 Aeneas와 Verus로 검증했으며, 검증기와 배포는 바이트 단위 재구성을 통해 대조 확인했다. 이중 지불과 가치 보존은 Lean 정리에 의해 기계 검증되었다.
검증 과정에서 총 6건의 문제가 발견되었으며, 그중 3건은 검증 도구 자체에서 발생했다. 팀은 여전히 의존하고 있는 가정도 함께 밝혔다. 해시의 충돌 없음, 검증기가 위조 증명을 거부한다는 점, 컨트랙트 동작이 모델과 일치한다는 점이다.
