15,000 lines of verified cryptography now in Python

Original Article ↗ Hacker News Discussion ↗

What Changed

  • CPython’s hashlib/HMAC implementations are being switched from OpenSSL (and other ad‑hoc code) to HACL*, a formally verified cryptographic library.
  • HACL* code is proved memory‑safe, functionally correct, and designed to avoid major timing/memory side channels.
  • The change is a drop‑in: Python code using the standard crypto APIs doesn’t need modification.

Performance and Safety

  • Main goal is safety; however, performance is also treated as a hard requirement for deployment.
  • Reported performance for replaced algorithms is similar or better; Blake2 specifically became faster due to more optimized code and proper CPU feature detection.
  • Some note that constant‑time, side‑channel‑resistant code can be slower, but prior code already aimed at this, so a big regression isn’t expected.

Formal Verification Debates

  • Supporters emphasize that formal proofs in F* are machine‑checked and far stronger than tests or dynamic typing, likening them to “static types on steroids.”
  • Skeptics argue large proofs (15k LOC of verified code) are likely to contain mistakes somewhere and that “verified” shouldn’t imply absolute trust; it reduces classes of bugs but doesn’t cover everything (e.g., algorithm choice, higher‑level protocol flaws).

Lines-of-Code and Dependency Concerns

  • Some criticize “15,000 lines” as a boastful or poor metric; others say it’s just conveying scope/coverage and implementation complexity.
  • Worry that Python now “depends on Microsoft” is countered by pointing out HACL*’s permissive licensing and the fact CPython vendors the generated C; there’s no runtime tie to Microsoft tooling.

Implementation Details

  • Crypto primitives are written and verified in F*/Low*, then compiled to C with KaRaMeL; a paper is cited claiming the F*→C translation preserves semantics and side‑channel properties.
  • During integration, a missing treatment of allocation failures in the original library was discovered and addressed, illustrating that verification has boundaries (it proves certain properties, not “everything”).

Python Versioning and Ecosystem Impact

  • The new crypto backend lands in Python 3.14, not earlier maintained versions.
  • Some argue it should be treated as a security hardening fix and backported; others note Python’s policy and the difficulty.
  • Significant discussion highlights how many popular libraries lag on supporting new Python releases, and that minor Python versions frequently introduce breaking changes, creating friction and long upgrade delays.

Broader Cryptography and Society

  • Tangential debate covers: modern crypto being “practically unbreakable” vs. risk of backdoors and implementation flaws, focus shifting from link‑level interception to endpoint compromise, and regulatory/attestation pressures limiting users’ ability to deploy secure software.

Open / Unclear Points

  • Whether this work will expand stdlib features (e.g., streaming SHAKE output) remains unclear; related issues are currently closed as “not planned.”
  • Reusability of the new streaming verification framework beyond hashes is raised but not substantively answered.