Search results

Learn from CBMC specification bug #985

Status: Open.

#986 In pq-code-package/mldsa-native;

· hanno-becker opened on Mar 3, 2026

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

hol-light

x86_64

Status: Open.

#982 In pq-code-package/mldsa-native;

· mkannwischer opened on Mar 2, 2026

Inconsistent and possibly confusing mld_sign() API and contracts

Status: Open.

#974 In pq-code-package/mldsa-native;

· rod-chapman opened on Feb 23, 2026

HOL-Light/AArch64: Port proofs from mlkem-native

aarch64

hol-light

Status: Open.

#949 In pq-code-package/mldsa-native;

· hanno-becker opened on Feb 5, 2026

·  

next

Config flag to only build for signature verification

Status: Open.

#941 In pq-code-package/mldsa-native;

· flynd opened on Feb 3, 2026

·  

next

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

Status: Open.

#936 In pq-code-package/mldsa-native;

· hanno-becker opened on Feb 2, 2026

·  

next

AVX2: Replace intrinsics implementation of rej_uniform_eta with assembly

x86_64

Status: Open.

#927 In pq-code-package/mldsa-native;

· mkannwischer opened on Jan 28, 2026

·  

next

AVX2: Replace intrinsics implementation of rej_uniform with assembly

x86_64

Status: Open.

#926 In pq-code-package/mldsa-native;

· mkannwischer opened on Jan 28, 2026

·  

next

AVX2: Replace intrinsics implementation of polyz_unpack with assembly

x86_64

Status: Open.

#925 In pq-code-package/mldsa-native;

· mkannwischer opened on Jan 28, 2026

·  

next

HOL-Light: Prove AArch64 rej_uniform_eta

aarch64

hol-light

Status: Open.

#924 In pq-code-package/mldsa-native;

· mkannwischer opened on Jan 28, 2026

HOL-Light: Prove AArch64 rej_uniform

aarch64

hol-light

Status: Open.

#923 In pq-code-package/mldsa-native;

· mkannwischer opened on Jan 28, 2026

HOL-Light: Prove AArch64 poly_decompose

aarch64

hol-light

Status: Open.

#922 In pq-code-package/mldsa-native;

· mkannwischer opened on Jan 28, 2026