Bài viết dưới đây trình bày kết quả đánh giá về tính đúng đắn của mô tả thuật toán, cũng như cài đặt của nó dưới góc nhìn chứng minh hình thức cho hai trong số các thuật toán lọt vào vòng 3 của quá trình chuẩn hóa thuật toán mật mã hậu lượng tử của NIST.