I disagree. SPARK is all about using formal methods to statically prove software properties. Clippy seems more comparable to parts of AdaCore's other static ana

I disagree. SPARK is all about using formal methods to statically prove software properties. Clippy seems more comparable to parts of AdaCore's other static analysis toolset (gnatsas). See https://docs.adacore.com/live/wave/gnatsas/html/user_guide/faq.html#what-is-the-difference-between-gnat-sas-and-spark https://docs.adacore.com/live/wave/gnatsas/html/user_guide/f...