diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..c4a847d
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/result
diff --git a/default.adc b/default.adc
new file mode 100644
index 0000000..c4a1e03
--- /dev/null
+++ b/default.adc
@@ -0,0 +1 @@
+pragma SPARK_Mode (On);
diff --git a/default.gpr b/default.gpr
new file mode 100644
index 0000000..7437fd5
--- /dev/null
+++ b/default.gpr
@@ -0,0 +1,14 @@
+project Default is
+
+   for Main use ("main");
+   for Source_Dirs use ("src");
+
+   package Builder is
+      for Global_Configuration_Pragmas use "default.adc";
+   end Builder;
+
+   package Compiler is
+      for Switches ("Ada") use ("-gnat2022");
+   end Compiler;
+
+end Default;
diff --git a/default.nix b/default.nix
new file mode 100644
index 0000000..6cb0bac
--- /dev/null
+++ b/default.nix
@@ -0,0 +1,40 @@
+with import <nixpkgs> { };
+
+stdenv.mkDerivation rec {
+  pname = "spark_fs_drivers";
+  version = "0.0.0";
+
+  src = ./.;
+
+  nativeBuildInputs = [
+    gnat
+    gprbuild
+    spark2014
+    z3
+  ];
+
+  gprFile = "default.gpr";
+
+  dontConfigure = true;
+
+  buildPhase = ''
+    runHook preBuild
+
+    gprbuild -P ${gprFile}
+    gnatprove -P ${gprFile} --prover=z3
+
+    runHook postBuild
+  '';
+
+  installPhase = ''
+    runHook preInstall
+
+    mkdir -p $out/bin
+    gprinstall --prefix=$out ${gprFile} \
+      --no-project \
+      --no-manifest \
+      --mode=usage
+    
+    runHook postInstall
+  '';
+}
diff --git a/src/a.out b/src/a.out
new file mode 100755
index 0000000..f410633
--- /dev/null
+++ b/src/a.out
Binary files differ
diff --git a/src/fs-filo.adb b/src/fs-filo.adb
new file mode 100644
index 0000000..3280b34
--- /dev/null
+++ b/src/fs-filo.adb
@@ -0,0 +1,22 @@
+package body FS.FILO is
+
+   procedure Read
+      (Buffer    : in out Buffer_Type;
+       Offset    : in     Natural;
+       Bytes_Read:    out Natural)
+   is
+      Sector_Size : constant Natural := 512;
+      Sector      : constant Interfaces.C.unsigned_long := Offset / Sector_Size;
+      Byte_Offset : constant Interfaces.C.unsigned_long := Offset rem Sector_Size;
+      Byte_Len    : constant Interfaces.C.unsigned_long := Buffer'Length;
+   begin
+
+      Bytes_Read := C_devread
+         (sector => Sector,
+          byte_offset => Byte_Offset,
+          byte_len => Byte_Len,
+          buf => Buffer'Address);
+   end Read;
+
+end FS.FILO;
+
diff --git a/src/fs-filo.ads b/src/fs-filo.ads
new file mode 100644
index 0000000..43b6cef
--- /dev/null
+++ b/src/fs-filo.ads
@@ -0,0 +1,31 @@
+with Interfaces.C;
+
+package FS.FILO is
+
+   Procedure Read
+      (Buffer  : in out Buffer_Type;
+       Offset  : in     Natural;
+       Success :    out Boolean);
+
+private
+
+   function C_devread
+      (sector : Interfaces.C.unsigned_long;
+       byte_offset : Interfaces.C.unsigned_long;
+       byte_len : Interfaces.C.unsigned_long;
+       buf : ... )
+      return Interfaces.C.int
+      with
+         SPARK_Mode => Off,
+         Import => True,
+         Conversion => C;
+   
+
+end FS.FILO;
+
+
+
+-- int mount (void)
+-- int read (char* buf, int len)
+-- int dir (char *dirname)
+-- void close (void) // not implemented
diff --git a/src/fs.ads b/src/fs.ads
new file mode 100644
index 0000000..3ea5a69
--- /dev/null
+++ b/src/fs.ads
@@ -0,0 +1,5 @@
+package FS is
+
+   type Buffer is array (Natural range <>) of Unsigned_8;
+
+end FS;
diff --git a/src/fs.c b/src/fs.c
new file mode 100644
index 0000000..271662a
--- /dev/null
+++ b/src/fs.c
@@ -0,0 +1,62 @@
+
+#include <stdio.h>
+
+#include "fs.h"
+
+FILE* block_device = NULL
+size_t device_size = 0;
+
+
+int devopen(const char* name, int* reopen)
+{
+	block_device = fopen(name, "rwb");
+	if (!block_device) {
+		return 0;
+	}
+	fseek(block_device, 0, SEEK_END)
+	return 1;
+}
+
+
+void devclose(void)
+{
+	if (block_device)
+		fclose(block_device);
+	block_device = NULL;
+	device_size = 0;
+}
+
+int devread(unsigned long sector, unsigned long byte_offset, unsigned long byte_len, void *buf)
+{
+	if (!block_device) {
+		fprintf(stdcerr, "devread: Device not open.\n");
+		return 0;
+	}
+
+	const unsigned long offset = sector * 512 + byte_offset;
+	if (offset + byte_len > device_size)
+		fprintf(stdcerr, "devread: Attempt to read beyond device.\n");
+		return 0;
+	}
+
+	if fseek(block_device, sector * 512 + byte_offset, SEEK_SET);
+	if (fread(buf, byte_len, 1, block_device) != byte_len) {
+		fprintf(stdcerr, "devread: Failed to read from device.\n");
+		return 0;
+	}
+	return 1;
+}
+
+
+
+//void dev_set_partition(unsigned long start, unsigned long size);
+//void dev_get_partition(unsigned long *start, unsigned long *size);
+
+//int file_open(const char *filename);
+//int file_read(void *buf, unsigned long len);
+//unsigned long file_seek(unsigned long offset);
+//unsigned long file_size(void);
+//void file_set_size(unsigned long size);
+//void file_close(void);
+
+#endif /* FS_H */
diff --git a/src/fs.h b/src/fs.h
new file mode 100644
index 0000000..cf7f003
--- /dev/null
+++ b/src/fs.h
@@ -0,0 +1,39 @@
+#ifndef FS_H
+#define FS_H
+
+/** devopen
+ * @param name    Filename to be used as blockdevice
+ * @param reopen  Unused, set NULL
+ * @return        1 on success, 0 on failure !CAUTION
+ */
+int devopen(const char *name, int *reopen);
+
+/** devclose
+ */
+void devclose(void);
+
+/** devread
+ * @param sector       512 byte sector of the block device
+ * @param byte_offset  Offset in the block
+ * @param byte_len     Buffer length
+ * @param buf          Buffer
+ * @return             1 on sucess, 0 on failure !CAUTION
+ */
+int devread(unsigned long sector, unsigned long byte_offset,
+	unsigned long byte_len, void *buf);
+
+
+
+
+
+void dev_set_partition(unsigned long start, unsigned long size);
+void dev_get_partition(unsigned long *start, unsigned long *size);
+
+int file_open(const char *filename);
+int file_read(void *buf, unsigned long len);
+unsigned long file_seek(unsigned long offset);
+unsigned long file_size(void);
+void file_set_size(unsigned long size);
+void file_close(void);
+
+#endif /* FS_H */
diff --git a/src/main.c b/src/main.c
new file mode 100644
index 0000000..91a40d7
--- /dev/null
+++ b/src/main.c
@@ -0,0 +1,22 @@
+#include <stdio.h>
+
+
+int main(int argc, char* argv[])
+{
+	if (argc != 2) {
+		fprintf(stdcerr, "Use %s /path/to/filesystem\n", argv[0]);
+		return -1;
+	}
+
+	if (devopen(argv[1], NULL) != 1) {
+		fprintf(stdcerr, "Faild to open %s\n", argv[1]);
+		return -1;
+	}
+
+	// TODO
+
+
+	devclose();
+	return 0;
+}
+