Blockstream on Nostr: Using LLMs to find bugs is well trodden. Using them to help prove a cryptographic ...

Using LLMs to find bugs is well trodden. Using them to help prove a cryptographic library correct is not.

Proof of concept from Jonas Nick, Director of Blockstream Research, with remix7531.

https://delvingbitcoin.org/t/libshrincs-a-c-implementation-with-a-machine-checked-security-proof/2795