I recently used Ada (not the SPARK subset) to develop an assembler/simulator (for a made-up ISA) for a computer architecture course I was taking. I used the Gtk

I recently used Ada (not the SPARK subset) to develop an assembler/simulator (for a made-up ISA) for a computer architecture course I was taking. I used the GtkAda bindings for the GUI, which worked well: https://github.com/docandrew/YOTROC https://github.com/docandrew/YOTROC I'm using SPARK for another project, and I think it's great. I don't think there is really an easier way of writing formally-verified software right now. Depending on the pre-conditions and post-conditions you put on your code, it can offer much stronger guarantees than other general-purpose programming languages do, but _proving_ those guarantees can be tricky if you don't have much experience with it. The nice thing about SPARK is that if you get something you can't prove (either because it's not legal SPARK or because the solver can't figure it out), you can turn off SPARK mode on a per-function or per-package basis and either come back to it later, or just prove that callers to the function abide by the specification without the function body itself being legal SPARK. For IDEs, I prefer VSCode over AdaCore's GPS IDE; AdaCore has a VSCode LSP plugin that I use: https://github.com/AdaCore/ada_language_server https://github.com/AdaCore/ada_language_server. Having said that, I used the GPS IDE for the computer architecture project and it worked well. Good luck!