Embed Notice

@hannesm @djm We did something like this for IKEv2 with TKM, which is part of strongSwan. (Library) Code generator which includes FSM and SPARK proof aspects for state transitions.

https://codelabs.ch/tkm/

@senier et al (now at AdaCore) has done a project called RecordFlux, which does much more: you can specify the protocol in a DSL and the tools will generate SPARK code with some formal guarantees. NVIDIA has actually used it in production.
Also, the code is opensource and up on GitHub.