New Product: AdaCore RecordFlux
We are excited that AdaCore has released a new product that will make working with binary communication protocols less effort and significantly more secure. With RecordFlux you define your binary protocols using a Domain Specific Language (DSL) and then automatically generate secure and verifiable Ada SPARK code to integrate into your application.
A case study performed by NVIDIA showed that from a 3,000 line protocol specification, 135,000 lines of mathematically verifiable Ada SPARK code was generated for sending and receiving binary protocol data. The resulting binary library was only 35kb, well within specification of the embedded system NVIDIA was targeting.
