TSC members:
Other attendees:
OQS update (Basil)
Basil gave his first update as the new OQS representative on the TSC. OQS is preparing a new release (the last release was in November 2025). This will be the first release to include mldsa-native code, replacing the previous PQ Crystals upstream. It will also include the new mlkem-native v1.1 release. Other highlights: adding MQOM (NIST PQC on-ramp signature submission), an update to NTRUPrime (still used by OpenSSH), and improved testing including Wycheproof test vectors for ML-KEM and ML-DSA. Release candidate expected by end of March.
PQCA/TAC update (Matthias)
Mentorship program: The call for proposals has been extended until mid-April since no proposals were submitted during the initial period. TAC chair elections and general member representative elections are ongoing. Matthias nominated himself again for the technical community representative and got confirmed. The group also briefly discussed OpenSSF baseline and its potential relevance to PQCA projects.
mlkem-libjade (Manuel)
A lot of work was done leading up to RWC. Improvements to repository maintenance and CI. New releases of the Jasmin compiler and an upcoming release of the EasyCrypt prover. A new release of mlkem-libjade is expected soon. Work on ML-DSA full proof is ongoing, with the goal of finishing before the end of the year.
mlkem-native (Matthias)
New release v1.1 with a PR into OQS. The biggest milestone is the completion of all HOL Light proofs for the x86 backend: correctness proofs, constant-time proofs, and memory safety proofs for all assembly. Intrinsic implementations were replaced with assembly to enable HOL Light verification. A new document SOUNDNESS.md has been added describing the verification approach, gaps, risks, and mitigations. The RWC talk was well received and generated interest from potential consumers.
mldsa-native (Matthias)
Ongoing HOL Light proofs for the Arm and x86 backends, with many functions still to cover. The goal is to complete verification and create a stable release (currently alpha) well before end of year. The x86 and Aarch64 verification are progressing in parallel. The C code is production-ready despite the alpha label. There is a memory-optimized configuration flag for ML-DSA that reduces RAM usage from ~130KB to much less, which could be added to OQS, but some CBMC proofs are not yet complete for that configuration due to issues with unions.
Basil asked about a pending PowerPC64 backend pull request for mlkem-native. Matthias will respond after consulting with Hanno.
TSC chair elections
Matthias’s term as TSC chair ends in April 2026. Proposed schedule:
The TSC approved this proposed schedule.
PQCP inclusion proposal: C++20 ML-KEM and ML-DSA (#204)
Anjan Roy presented his proposal to include two C++20 libraries (ML-KEM and ML-DSA) in PQCP. The libraries are header-only, fully constexpr, use std::span instead of raw pointers, have zero dependencies, and are portable (no assembly). Performance is approximately 3x slower than mlkem-native/mldsa-native (compared against assembly backends), primarily due to lack of 4x SIMD parallel Keccak hashing. The libraries have extensive testing (property-based, mutation, fuzzing) and strict compiler/static analysis settings.
Discussion points:
constexpr features which are not available in C.The TSC agreed to continue the discussion on GitHub for one week, then Matthias will call for a vote via the LFX platform (rather than GitHub issues) to improve participation.
Reconsider TSC meetings (#193)
The current approach of opening a GitHub issue before each meeting to check attendance and canceling if fewer than 4 people plan to attend is working well. The TSC agreed to continue this practice.
Growth plan and documentation standards
The growth plan (#188) and documentation standards (#151) have been completed by the sub-projects represented at the meeting (mlkem-native, mldsa-native, mlkem-libjade) but remain outstanding for rust-libcrux and slhdsa-c.