Generation > record-flux

RecordFlux: Toolset for the formal specification of messages and the generation of verifiable binary parsers and message generators in SPARK.