Formal verification is the act of proving the correctness of software using mathematics. That means proving that your code is free of bugs and/or follows its specifications. SPARK is both a language (subset of Ada) and a set of tools that bring automatic formal verification in the hands of any developer.

This technology is getting more interest from the industry (e.g. NVIDIA recently) for its extremely powerful properties in terms of safety and security. However, it is not widely known that SPARK is both open source and very easy to start using.

In this talk I will provide quick and easy instructions to start your first formally verified library in SPARK. Using only free and open-source tools and resources (compiler, package manager, IDE, verification tools).