https://en.wikipedia.org/wiki/Formal_verification

Provable correctness is important in many different application contexts, especially cryptography. The benefit for Python (and for any other user of the library in question) is fewer bugs and thus greater security assurance.

If you look at the original bug that spawned this work (https://github.com/python/cpython/issues/99108), the poster reported:

"""As evidenced by the recent SHA3 buffer overflow, cryptographic primitives are tricky to implement correctly. There might be issues with memory management, exceeding lengths, incorrect buffer management, or worse, incorrect implementations in corner cases.

The HACL* project https://github.com/hacl-star/hacl-star provides verified implementations of cryptographic primitives. These implementations are mathematically shown to be:

    memory safe (no buffer overflows, no use-after-free)
    functionally correct (they always compute the right result)
    side-channel resistant (the most egregious variants of side-channels, such as memory and timing leaks, are ruled out by construction)."""