# Win32\_Hash\_Argon2 password hashing in Spark

**URL:** https://forum.ada-lang.io/t/win32-hash-argon2-password-hashing-in-spark/4873
**Category:** Releases
**Tags:** spark
**Created:** [October 21, 2026, 1:52am UTC](https://forum.ada-lang.io/t/win32-hash-argon2-password-hashing-in-spark/4873 "2026-10-21T01:52:42Z")
**Posts on this page:** 1
**Page:** 1

<div class="post-metadata">

### Author: ![Avila](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/avila/32/1100_2.png) [@Avila](https://forum.ada-lang.io/u/Avila)
#### Post date: [October 21, 2026, 1:52am UTC](https://forum.ada-lang.io/t/win32-hash-argon2-password-hashing-in-spark/4873/1 "2026-10-21T01:52:42Z")

</div>

**Hi all,**

I’ve published a companion Windows password-hashing library in Ada/SPARK: Win32\_Hash\_Argon2.

What it does:

- **Argon2id** password hashing and verification, wrapping the native C library under a rigorous SPARK compliant architecture.

- Random salt generation via Windows `ProcessPrng` with `BCryptGenRandom` as an automatic cryptographic fallback.

- Standard encoded hash output supporting configurable cost parameters (_t-cost_, _m-cost_, parallelism) and strict format validation.

- Separate verify procedure built on a strict **fail-closed / fail-stop** pattern.

- **Memory sanitization:** Every secret (`Password`, `Salt`, temporary hashes) is aggressively wiped using `SecureZeroMemory` plus a redundant Ada overwrite on success and across **every single** exceptional exit path (entropy failures, range/constraint errors, API faults, or unexpected exceptions).

Verification:

- **GNATprove :** all provers: 28/28 checks proved, 0 unproved.

- **Verified on two Gnatprove version: Community 2021, 16.1.0**

Honest scope: The low-level bindings interfacing directly with the Windows API and the external Argon2 C library are `SPARK_Mode => Off`, while all surrounding wrapper logic, state validation, and safety invariants are formally proved. Windows only.

Apache-2.0: [GitHub - EliAvila10/Win32\_Hash\_Argon2 · GitHub](https://github.com/EliAvila10/Win32_Hash_Argon2)

Feedback welcome.