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