diff --git a/resources/templates/spark_main/example.yaml b/resources/templates/spark_main/example.yaml
new file mode 100644
index 0000000..5cc4d4d
--- /dev/null
+++ b/resources/templates/spark_main/example.yaml
@@ -0,0 +1,3 @@
+name: SPARK Main
+description: Simple overrideable provable main
+main: main
diff --git a/resources/templates/spark_main/main.adb b/resources/templates/spark_main/main.adb
new file mode 100644
index 0000000..e0d8401
--- /dev/null
+++ b/resources/templates/spark_main/main.adb
@@ -0,0 +1,4 @@
+procedure Main is
+begin
+   null;
+end Main;
diff --git a/resources/templates/spark_main/main.adc b/resources/templates/spark_main/main.adc
new file mode 100644
index 0000000..6a07ed7
--- /dev/null
+++ b/resources/templates/spark_main/main.adc
@@ -0,0 +1,6 @@
+
+pragma Profile(GNAT_Extended_Ravenscar);
+pragma Partition_Elaboration_Policy(Sequential);
+pragma SPARK_Mode (On);
+pragma Warnings (Off, "no Global contract available");
+pragma Warnings (Off, "subprogram * has no effect");
diff --git a/resources/templates/spark_main/main.gpr b/resources/templates/spark_main/main.gpr
new file mode 100644
index 0000000..7e52d62
--- /dev/null
+++ b/resources/templates/spark_main/main.gpr
@@ -0,0 +1,15 @@
+project Main is
+
+   for Main use ("main.adb");
+
+   package Compiler is
+      for Switches ("ada") use ("-g", "-gnatwa", "-gnatQ");
+   end Compiler;
+
+   package Builder is
+      for Switches ("ada") use ("-g", "-O0");
+
+      for Global_Configuration_Pragmas use "main.adc";
+   end Builder;
+
+end Main;