Issues · pq-code-package/mldsa-native · GitHub

Labels Milestones New issue

Signing: Combine `mld_poly_make_hint` and `mld_pack_sig_h_poly`

#1027

· mkannwischer opened

on Apr 8, 2026

CBMC: Eliminate proof performance workaround in signing

#1026

· mkannwischer opened

on Apr 8, 2026

HOL-Light: Port AArch64 Keccak safety proofs from mlkem-native

#1023

· mkannwischer opened

on Apr 6, 2026

HOL-Light: Use pairwise nonoverlapping clause to improve spec readability

#1018

· hanno-becker opened

on Apr 5, 2026

HOL-Light: Add safety and constant-time proofs

#1001

· mkannwischer opened

on Mar 21, 2026

HOL-Light: Unify "pre-conditions as post-conditions" style

#995

· hanno-becker opened

on Mar 16, 2026

HOL-Light: Unify specification-style for arithmetic arrays

#994

· hanno-becker opened

on Mar 16, 2026

Learn from CBMC specification bug #985

#986

· hanno-becker opened

on Mar 3, 2026

Port HOL-Light/x86_64: Replace Keccakx4 intrinsics with assembly and prove correct

#982

· mkannwischer opened

on Mar 2, 2026

Inconsistent and possibly confusing mld_sign() API and contracts

#974

· rod-chapman opened

on Feb 23, 2026

Config flag to only build for signature verification

#941

· flynd opened

on Feb 3, 2026

·

Ensure that all non-static symbols are guarded by MLD_CONFIG_{INTERNAL/EXTERNAL}_API_QUALIFIER

#936

· hanno-becker opened

on Feb 2, 2026

·