I've released a new version of CoAP_SPARK, my formally verified implementation of this IoT protocol. The implementation language is SPARK, the verifiable subset of Ada. https://github.com/mgrojo/coap_spark