LLMs are used very successfully to find vulnerabilities in Bitcoin software.
Can they also help prove the security of a modern cryptographic library for Bitcoin?
To explore this question,
@remix7531 and I are publishing libshrincs.
libshrincs is a handwritten C library implementing WOTS+C, the one-time signature used by SHRINCS.
It is a proof of concept and should not be used in production.
Its machine-checked proofs connect the C implementation to an unforgeability theorem.
The current theorem does not yet give a full post-quantum security bound.
The post and review tutorial describe its current limits.
Code and proofs:
Review tutorial for the security proof (no Rocq or SSProve background required):
@remix7531 has written three excellent posts on the library and verification work:
Towards libshrincs
The grind was the only detector
Choosing a verification toolchain