모나쉬대와 ExeQuantum 연구진이 ML-KEM의 수론적 변환(NTT)을 Plantard 산술 기반으로 형식 검증하는 코드 생성기를 제시했다. 이 생성기는 정적 경계 분석기를 내장해 런타임 분기 없이 코드 생성 시점에 모듈러 리덕션을 배치하며, 단일 파라미터 조합으로 ML-KEM·ML-DSA·FN-DSA를 모두 대상으로 하는 구조적으로 동일한 C 코드와 형식 검증용 Jasmin 코드를 동시에 생성한다. EasyCrypt로 Plantard 산술을 정형화하고 추출된 Jasmin NTT와 기존 formosa-mlkem 명세 간 계층별 프로그램 등가성을 증명해 수학적 NTT 정의까지 정확성을 확장했다. 벤치마크 결과 생성된 코드는 참조 C 구현 대비 순방향 NTT에서 1.5~1.8배, 역방향에서 1.7~2.5배 빨랐고, 기존 형식 검증된 formosa-mlkem Jasmin 구현보다도 ML-KEM에서 최대 2.19배 빠른 성능을 보였다. 격자 기반 암호의 성능과 형식 검증을 동시에 만족시키는 실용적 접근으로 다른 격자 산술 프리미티브에도 일반화될 수 있을 것으로 기대된다.

• •모나쉬대·ExeQuantum 연구진, ML-KEM NTT의 형식 검증된 코드 생성기 제안
• •정적 경계 분석기로 런타임 분기 없이 모듈러 리덕션 배치, 수동 튜닝 불필요
• •EasyCrypt 기반 Plantard 산술 정형화 및 계층별 프로그램 등가성 증명으로 정확성 보장
• •순방향 NTT 1.5~1.8배, 역방향 1.7~2.5배 성능 향상, 기존 형식검증 구현 대비 최대 2.19배 개선
• •격자 기반 암호의 다른 프리미티브에도 일반화 가능한 성능·검증 동시 달성 기법 제시