Issues

• Add CI job to check links

  GaloisInc/cryptol-specs#349 · Filter by author marsella opened on May 8, 2026

• Revisit X25519 location and docs

  GaloisInc/cryptol-specs#304 · Filter by author marsella opened on Jun 3, 2025

• Validate WOTS+ implementation

  bug
  Bug

  GaloisInc/cryptol-specs#303 · Filter by author amaloz opened on May 28, 2025
  3

  

• Primitive::Asymmetric::Signature::WOTS::Instantiations::WOTSP_SHA2_25::WOTSisCorrect takes an extraordinarily long time to :check

  GaloisInc/cryptol-specs#301 · Filter by author RyanGlScott opened on May 21, 2025

• Add CI job to run SAW proofs

  CI
  GaloisInc/cryptol-specs#297 · Filter by author marsella opened on May 2, 2025

• Bring RSA primitives up to gold standard

  GaloisInc/cryptol-specs#293 · Filter by author marsella opened on Apr 23, 2025
  

• Add IKE v2 KDFs

  GaloisInc/cryptol-specs#267 · Filter by author marsella opened on Apr 1, 2025
  3

• Add KDFs from SP 800-135

  new-spec
  GaloisInc/cryptol-specs#266 · Filter by author marsella opened on Mar 26, 2025
  1

• Expand HashInterface to support HMAC

  GaloisInc/cryptol-specs#256 · Filter by author marsella opened on Mar 11, 2025
  3

• Review common code

  improvement
  GaloisInc/cryptol-specs#236 · Filter by author marsella opened on Feb 4, 2025

• ML-DSA: Add properties of sampling functions

  CNSA 2.0good first issueimprovement
  GaloisInc/cryptol-specs#207 · Filter by author marsella opened on Dec 11, 2024

• Primitive::Asymmetric::Cipher::RSA's IntegerRSACorrectKeyGen property take an extraordinarily long time to :check

  GaloisInc/cryptol-specs#204 · Filter by author RyanGlScott opened on Dec 9, 2024

• ML-DSA: Define HashML-DSA external functions

  CNSA 2.0version-update
  GaloisInc/cryptol-specs#199 · Filter by author marsella opened on Dec 2, 2024

• XMSS: Outline and implement XMSS^MT

  GaloisInc/cryptol-specs#178 · Filter by author marsella opened on Nov 11, 2024

• XMSS: Implement keys and functions on keys

  GaloisInc/cryptol-specs#176 · Filter by author marsella opened on Nov 11, 2024
  

• Update type-check CI to include literate specs

  CIgood first issue
  GaloisInc/cryptol-specs#168 · Filter by author mccleeary-galois opened on Oct 31, 2024
  1

• Properties only working on particular Z3 versions

  buggood first issue
  GaloisInc/cryptol-specs#166 · Filter by author mccleeary-galois opened on Oct 31, 2024
  1

• :check katanCorrect fails

  bug
  GaloisInc/cryptol-specs#165 · Filter by author RyanGlScott opened on Oct 31, 2024

• Possibly incorrect definition of gostCorrect64

  bug
  GaloisInc/cryptol-specs#164 · Filter by author RyanGlScott opened on Oct 31, 2024
  1

• Consolidate and spec-ify NTT implementations

  GaloisInc/cryptol-specs#163 · Filter by author marsella opened on Oct 31, 2024
  3

• Deprecate old specs and update SHA3 API

  CNSA 2.0improvement
  GaloisInc/cryptol-specs#152 · Filter by author marsella opened on Oct 8, 2024
  3

• Abstract the sponge construction used in SHA3

  CNSA 2.0improvement
  GaloisInc/cryptol-specs#140 · Filter by author marsella opened on Sep 17, 2024
  2

• Expand ECDH test vectors

  improvementSuite-B
  GaloisInc/cryptol-specs#136 · Filter by author marsella opened on Sep 5, 2024

• Convert SHA-2 to be a literate spec

  CNSA 2.0literateSuite-B
  GaloisInc/cryptol-specs#134 · Filter by author marsella opened on Aug 30, 2024

• Consider adding more SHA2 test vectors

  good first issueimprovementSuite-B
  GaloisInc/cryptol-specs#130 · Filter by author marsella opened on Aug 29, 2024
  1