Hi Coq users! How can I make formally verified HTTP requests with Coq so I can make a formally verified Matrix bot? Is it possible?

Haven't tried it, but https://github.com/liyishuai/coq-http exists and might help. It won't be quick, but it might be lots of fun!

The cost might depend on what kind of formal verification you have in mind, and on how much Coq experience you already have.

Last updated: Jun 18 2024 at 20:02 UTC