A process for Ada/SPARK software to meet ISO 26262

Adventures for Learning and Inspiring Coding Excellence

Unbound data structures in Ada-Spark.

Minimalist cooperative operating system supporting multiple tasks with MMU protection

🚗 ADA Spark Car' Assistant Prototype for Formal Approches to software Engineer at Napier University

A universal, language-agnostic code analysis and verification engine. LLM-powered. Formal-methods-backed. Runtime-ready. Think mypy meets miri meets Coq—for any language.

A pilot assistance system for a plane written in the ADA SPARK language.

A collection of silver-level SPARK 2014 verified RFSB509 implementations, that deviate from the original specifications. This is for research only.

Coursework for the Formal Approaches to Software Engineering module taken in 4th year

Contains the practice work and code from lectures in the Formal Approaches to Software Engineering Module