I really enjoyed making this demo, let me know what you think and how you think I can make this a stronger message to advocate for SPARK.
One of my next steps is to analyze the C code with static analysis to see if I can find the same problems. Not sure if it would.
The full LinkedIn topic is here: AI Ports, Formal Methods Prove: Memory Safety on ST Micro Boards with SPARK | AdaCore
Like and subscribe!