diff --git a/src/interface/ffi/.zig-cache/o/a321aa3c8732663417bf1076929f850a/test b/src/interface/ffi/.zig-cache/o/a321aa3c8732663417bf1076929f850a/test
new file mode 100755
index 0000000..5860164
Binary files /dev/null and b/src/interface/ffi/.zig-cache/o/a321aa3c8732663417bf1076929f850a/test differ
diff --git a/src/interface/ffi/.zig-cache/o/a321aa3c8732663417bf1076929f850a/test.o b/src/interface/ffi/.zig-cache/o/a321aa3c8732663417bf1076929f850a/test.o
new file mode 100644
index 0000000..9cd1f36
Binary files /dev/null and b/src/interface/ffi/.zig-cache/o/a321aa3c8732663417bf1076929f850a/test.o differ
diff --git a/src/interface/ffi/.zig-cache/z/f584d7a82e773a8ccab74d110e816abc b/src/interface/ffi/.zig-cache/z/f584d7a82e773a8ccab74d110e816abc
new file mode 100644
index 0000000..aa0a4ce
Binary files /dev/null and b/src/interface/ffi/.zig-cache/z/f584d7a82e773a8ccab74d110e816abc differ
diff --git a/src/interface/ffi/src/main.zig b/src/interface/ffi/src/main.zig
index 6b233bc..b9f8cd1 100644
--- a/src/interface/ffi/src/main.zig
+++ b/src/interface/ffi/src/main.zig
@@ -1,274 +1,342 @@
-// {{PROJECT}} FFI Implementation
+// Alloyiser FFI Reference Implementation
 //
-// This module implements the C-compatible FFI declared in src/abi/Foreign.idr
-// All types and layouts must match the Idris2 ABI definitions.
+// Implements the C-ABI functions declared in
+// src/interface/abi/Alloyiser/ABI/Foreign.idr. The Idris2 ABI is the source of
+// truth: every `%foreign "C:alloyiser_*"` symbol and every Result code below
+// matches it exactly (symbol names, arity, and integer encodings).
+//
+// This is a self-contained reference: it builds an Alloy model in memory and
+// serialises it to .als / JSON. Real assertion analysis (the JVM/Alloy Analyzer
+// bridge) is future work; `alloyiser_analyze` reports no counterexamples.
 //
 // SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 const std = @import("std");
 
-// Version information (keep in sync with project)
 const VERSION = "0.1.0";
-const BUILD_INFO = "{{PROJECT}} built with Zig " ++ @import("builtin").zig_version_string;
-
-/// Thread-local error storage
-threadlocal var last_error: ?[]const u8 = null;
-
-/// Set the last error message
-fn setError(msg: []const u8) void {
-    last_error = msg;
-}
-
-/// Clear the last error
-fn clearError() void {
-    last_error = null;
-}
+const BUILD_INFO = "alloyiser built with Zig " ++ @import("builtin").zig_version_string;
 
 //==============================================================================
-// Core Types (must match src/abi/Types.idr)
+// Result Codes (must match Alloyiser.ABI.Types.resultToInt)
 //==============================================================================
 
-/// Result codes (must match Idris2 Result type)
 pub const Result = enum(c_int) {
     ok = 0,
-    @"error" = 1,
+    err = 1, // Idris `Error`
     invalid_param = 2,
     out_of_memory = 3,
     null_pointer = 4,
+    model_parse_error = 5,
+    solver_timeout = 6,
+    counterexample_found = 7,
 };
 
-/// Library handle (opaque to prevent direct access)
-pub const Handle = opaque {
-    // Internal state hidden from C
-    allocator: std.mem.Allocator,
-    initialized: bool,
-    // Add your fields here
-};
-
-//==============================================================================
-// Library Lifecycle
-//==============================================================================
-
-/// Initialize the library
-/// Returns a handle, or null on failure
-export fn {{project}}_init() ?*Handle {
-    const allocator = std.heap.c_allocator;
-
-    const handle = allocator.create(Handle) catch {
-        setError("Failed to allocate handle");
-        return null;
-    };
-
-    // Initialize handle
-    handle.* = .{
-        .allocator = allocator,
-        .initialized = true,
-    };
-
-    clearError();
-    return handle;
+fn code(r: Result) c_int {
+    return @intFromEnum(r);
 }
 
-/// Free the library handle
-export fn {{project}}_free(handle: ?*Handle) void {
-    const h = handle orelse return;
-    const allocator = h.allocator;
-
-    // Clean up resources
-    h.initialized = false;
+/// Thread-local last-error message (a static string; never freed by the caller).
+threadlocal var last_error: ?[*:0]const u8 = null;
 
-    allocator.destroy(h);
-    clearError();
+fn setError(msg: [*:0]const u8) void {
+    last_error = msg;
 }
 
 //==============================================================================
-// Core Operations
+// Model state
 //==============================================================================
 
-/// Process data (example operation)
-export fn {{project}}_process(handle: ?*Handle, input: u32) Result {
-    const h = handle orelse {
-        setError("Null handle");
-        return .null_pointer;
-    };
+const Sig = struct { name: []u8, is_abstract: bool, parent: []u8 };
+const Field = struct { owner: []u8, name: []u8, target: []u8, mult: u32 };
+const Named = struct { name: []u8, body: []u8 };
 
-    if (!h.initialized) {
-        setError("Handle not initialized");
-        return .@"error";
+/// An Alloy model under construction. Opaque to C (passed as a pointer).
+const Model = struct {
+    allocator: std.mem.Allocator,
+    module_name: []u8,
+    sigs: std.ArrayList(Sig),
+    fields: std.ArrayList(Field),
+    facts: std.ArrayList(Named),
+    assertions: std.ArrayList(Named),
+
+    fn deinit(self: *Model) void {
+        const a = self.allocator;
+        a.free(self.module_name);
+        for (self.sigs.items) |s| {
+            a.free(s.name);
+            a.free(s.parent);
+        }
+        self.sigs.deinit();
+        for (self.fields.items) |f| {
+            a.free(f.owner);
+            a.free(f.name);
+            a.free(f.target);
+        }
+        self.fields.deinit();
+        for (self.facts.items) |f| {
+            a.free(f.name);
+            a.free(f.body);
+        }
+        self.facts.deinit();
+        for (self.assertions.items) |x| {
+            a.free(x.name);
+            a.free(x.body);
+        }
+        self.assertions.deinit();
     }
+};
 
-    // Example processing logic
-    _ = input;
-
-    clearError();
-    return .ok;
+/// Duplicate a C string into an owned, non-sentinel byte slice.
+fn dup(a: std.mem.Allocator, s: ?[*:0]const u8) ![]u8 {
+    const slice: []const u8 = if (s) |p| std.mem.span(p) else "";
+    return a.dupe(u8, slice);
 }
 
 //==============================================================================
-// String Operations
+// Model lifecycle
 //==============================================================================
 
-/// Get a string result (example)
-/// Caller must free the returned string
-export fn {{project}}_get_string(handle: ?*Handle) ?[*:0]const u8 {
-    const h = handle orelse {
-        setError("Null handle");
+export fn alloyiser_model_create(module_name: ?[*:0]const u8) callconv(.C) ?*Model {
+    const a = std.heap.c_allocator;
+    const m = a.create(Model) catch {
+        setError("alloyiser: failed to allocate model");
         return null;
     };
-
-    if (!h.initialized) {
-        setError("Handle not initialized");
-        return null;
-    }
-
-    // Example: allocate and return a string
-    const result = h.allocator.dupeZ(u8, "Example result") catch {
-        setError("Failed to allocate string");
-        return null;
+    m.* = .{
+        .allocator = a,
+        .module_name = dup(a, module_name) catch {
+            a.destroy(m);
+            setError("alloyiser: failed to allocate module name");
+            return null;
+        },
+        .sigs = std.ArrayList(Sig).init(a),
+        .fields = std.ArrayList(Field).init(a),
+        .facts = std.ArrayList(Named).init(a),
+        .assertions = std.ArrayList(Named).init(a),
     };
-
-    clearError();
-    return result.ptr;
+    return m;
 }
 
-/// Free a string allocated by the library
-export fn {{project}}_free_string(str: ?[*:0]const u8) void {
-    const s = str orelse return;
-    const allocator = std.heap.c_allocator;
-
-    const slice = std.mem.span(s);
-    allocator.free(slice);
+export fn alloyiser_model_free(model: ?*Model) callconv(.C) void {
+    const m = model orelse return;
+    const a = m.allocator;
+    m.deinit();
+    a.destroy(m);
 }
 
 //==============================================================================
-// Array/Buffer Operations
+// Model construction
 //==============================================================================
 
-/// Process an array of data
-export fn {{project}}_process_array(
-    handle: ?*Handle,
-    buffer: ?[*]const u8,
-    len: u32,
-) Result {
-    const h = handle orelse {
-        setError("Null handle");
-        return .null_pointer;
+export fn alloyiser_add_sig(
+    model: ?*Model,
+    name: ?[*:0]const u8,
+    is_abstract: u32,
+    parent: ?[*:0]const u8,
+) callconv(.C) c_int {
+    const m = model orelse return code(.null_pointer);
+    const n = dup(m.allocator, name) catch return code(.out_of_memory);
+    const p = dup(m.allocator, parent) catch {
+        m.allocator.free(n);
+        return code(.out_of_memory);
     };
-
-    const buf = buffer orelse {
-        setError("Null buffer");
-        return .null_pointer;
+    m.sigs.append(.{ .name = n, .is_abstract = is_abstract != 0, .parent = p }) catch {
+        m.allocator.free(n);
+        m.allocator.free(p);
+        return code(.out_of_memory);
     };
+    return code(.ok);
+}
 
-    if (!h.initialized) {
-        setError("Handle not initialized");
-        return .@"error";
-    }
+export fn alloyiser_add_field(
+    model: ?*Model,
+    owner: ?[*:0]const u8,
+    field: ?[*:0]const u8,
+    target: ?[*:0]const u8,
+    mult: u32,
+) callconv(.C) c_int {
+    const m = model orelse return code(.null_pointer);
+    const o = dup(m.allocator, owner) catch return code(.out_of_memory);
+    const f = dup(m.allocator, field) catch {
+        m.allocator.free(o);
+        return code(.out_of_memory);
+    };
+    const t = dup(m.allocator, target) catch {
+        m.allocator.free(o);
+        m.allocator.free(f);
+        return code(.out_of_memory);
+    };
+    m.fields.append(.{ .owner = o, .name = f, .target = t, .mult = mult }) catch {
+        m.allocator.free(o);
+        m.allocator.free(f);
+        m.allocator.free(t);
+        return code(.out_of_memory);
+    };
+    return code(.ok);
+}
 
-    // Access the buffer
-    const data = buf[0..len];
-    _ = data;
+fn addNamed(list: *std.ArrayList(Named), a: std.mem.Allocator, name: ?[*:0]const u8, body: ?[*:0]const u8) c_int {
+    const n = dup(a, name) catch return code(.out_of_memory);
+    const b = dup(a, body) catch {
+        a.free(n);
+        return code(.out_of_memory);
+    };
+    list.append(.{ .name = n, .body = b }) catch {
+        a.free(n);
+        a.free(b);
+        return code(.out_of_memory);
+    };
+    return code(.ok);
+}
 
-    // Process data here
+export fn alloyiser_add_fact(model: ?*Model, name: ?[*:0]const u8, body: ?[*:0]const u8) callconv(.C) c_int {
+    const m = model orelse return code(.null_pointer);
+    return addNamed(&m.facts, m.allocator, name, body);
+}
 
-    clearError();
-    return .ok;
+export fn alloyiser_add_assertion(model: ?*Model, name: ?[*:0]const u8, body: ?[*:0]const u8) callconv(.C) c_int {
+    const m = model orelse return code(.null_pointer);
+    return addNamed(&m.assertions, m.allocator, name, body);
 }
 
 //==============================================================================
-// Error Handling
+// Analyzer (reference stub: no counterexamples)
 //==============================================================================
 
-/// Get the last error message
-/// Returns null if no error
-export fn {{project}}_last_error() ?[*:0]const u8 {
-    const err = last_error orelse return null;
+export fn alloyiser_analyze(model: ?*Model, scope: u32, timeout_ms: u32) callconv(.C) c_int {
+    _ = scope;
+    _ = timeout_ms;
+    if (model == null) return code(.null_pointer);
+    // Reference build performs no SAT solving; all assertions vacuously hold.
+    return code(.ok);
+}
 
-    // Return C string (static storage, no need to free)
-    const allocator = std.heap.c_allocator;
-    const c_str = allocator.dupeZ(u8, err) catch return null;
-    return c_str.ptr;
+export fn alloyiser_counterexample_count(model: ?*Model) callconv(.C) u32 {
+    if (model == null) return 0;
+    return 0;
 }
 
-//==============================================================================
-// Version Information
-//==============================================================================
+export fn alloyiser_counterexample_assertion(model: ?*Model, index: u32) callconv(.C) ?[*:0]const u8 {
+    _ = model;
+    _ = index;
+    return null;
+}
 
-/// Get the library version
-export fn {{project}}_version() [*:0]const u8 {
-    return VERSION.ptr;
+export fn alloyiser_counterexample_atom_count(model: ?*Model, index: u32) callconv(.C) u32 {
+    _ = model;
+    _ = index;
+    return 0;
 }
 
-/// Get build information
-export fn {{project}}_build_info() [*:0]const u8 {
-    return BUILD_INFO.ptr;
+export fn alloyiser_counterexample_describe(model: ?*Model, index: u32) callconv(.C) ?[*:0]const u8 {
+    _ = model;
+    _ = index;
+    return null;
 }
 
 //==============================================================================
-// Callback Support
+// Serialisation
 //==============================================================================
 
-/// Callback function type (C ABI)
-pub const Callback = *const fn (u64, u32) callconv(.C) u32;
-
-/// Register a callback
-export fn {{project}}_register_callback(
-    handle: ?*Handle,
-    callback: ?Callback,
-) Result {
-    const h = handle orelse {
-        setError("Null handle");
-        return .null_pointer;
-    };
-
-    const cb = callback orelse {
-        setError("Null callback");
-        return .null_pointer;
+fn multKeyword(mult: u32) []const u8 {
+    return switch (mult) {
+        0 => "one",
+        1 => "lone",
+        2 => "set",
+        else => "seq",
     };
+}
 
-    if (!h.initialized) {
-        setError("Handle not initialized");
-        return .@"error";
+fn renderAls(m: *Model) ![:0]u8 {
+    var buf = std.ArrayList(u8).init(m.allocator);
+    defer buf.deinit();
+    const w = buf.writer();
+    try w.print("module {s}\n\n", .{m.module_name});
+    for (m.sigs.items) |s| {
+        if (s.is_abstract) try w.writeAll("abstract ");
+        if (s.parent.len > 0) {
+            try w.print("sig {s} extends {s} {{", .{ s.name, s.parent });
+        } else {
+            try w.print("sig {s} {{", .{s.name});
+        }
+        var first = true;
+        for (m.fields.items) |f| {
+            if (std.mem.eql(u8, f.owner, s.name)) {
+                try w.print("{s}\n  {s}: {s} {s}", .{ if (first) "" else ",", f.name, multKeyword(f.mult), f.target });
+                first = false;
+            }
+        }
+        try w.writeAll(if (first) "}\n" else "\n}\n");
     }
+    for (m.facts.items) |f| try w.print("\nfact {s} {{ {s} }}\n", .{ f.name, f.body });
+    for (m.assertions.items) |x| try w.print("\nassert {s} {{ {s} }}\n", .{ x.name, x.body });
+    return buf.toOwnedSliceSentinel(0);
+}
 
-    // Store callback for later use
-    _ = cb;
+export fn alloyiser_model_to_als(model: ?*Model) callconv(.C) ?[*:0]const u8 {
+    const m = model orelse return null;
+    const out = renderAls(m) catch {
+        setError("alloyiser: failed to render .als");
+        return null;
+    };
+    return out.ptr;
+}
 
-    clearError();
-    return .ok;
+export fn alloyiser_model_to_json(model: ?*Model) callconv(.C) ?[*:0]const u8 {
+    const m = model orelse return null;
+    var buf = std.ArrayList(u8).init(m.allocator);
+    defer buf.deinit();
+    const w = buf.writer();
+    w.print("{{\"module\":\"{s}\",\"sigs\":{d},\"fields\":{d},\"facts\":{d},\"assertions\":{d}}}", .{ m.module_name, m.sigs.items.len, m.fields.items.len, m.facts.items.len, m.assertions.items.len }) catch {
+        setError("alloyiser: failed to render JSON");
+        return null;
+    };
+    const out = buf.toOwnedSliceSentinel(0) catch return null;
+    return out.ptr;
 }
 
 //==============================================================================
-// Utility Functions
+// String / error helpers
 //==============================================================================
 
-/// Check if handle is initialized
-export fn {{project}}_is_initialized(handle: ?*Handle) u32 {
-    const h = handle orelse return 0;
-    return if (h.initialized) 1 else 0;
+export fn alloyiser_free_string(str: ?[*:0]const u8) callconv(.C) void {
+    const p = str orelse return;
+    std.heap.c_allocator.free(std.mem.span(p));
+}
+
+export fn alloyiser_last_error() callconv(.C) ?[*:0]const u8 {
+    return last_error;
+}
+
+export fn alloyiser_version() callconv(.C) [*:0]const u8 {
+    return VERSION;
+}
+
+export fn alloyiser_build_info() callconv(.C) [*:0]const u8 {
+    return BUILD_INFO;
 }
 
 //==============================================================================
 // Tests
 //==============================================================================
 
-test "lifecycle" {
-    const handle = {{project}}_init() orelse return error.InitFailed;
-    defer {{project}}_free(handle);
-
-    try std.testing.expect({{project}}_is_initialized(handle) == 1);
-}
+test "model lifecycle and serialisation" {
+    const m = alloyiser_model_create("univ") orelse return error.CreateFailed;
+    defer alloyiser_model_free(m);
 
-test "error handling" {
-    const result = {{project}}_process(null, 0);
-    try std.testing.expectEqual(Result.null_pointer, result);
+    try std.testing.expectEqual(code(.ok), alloyiser_add_sig(m, "Node", 0, ""));
+    try std.testing.expectEqual(code(.ok), alloyiser_add_field(m, "Node", "next", "Node", 1));
+    try std.testing.expectEqual(code(.ok), alloyiser_add_assertion(m, "acyclic", "no n: Node | n in n.^next"));
+    try std.testing.expectEqual(code(.ok), alloyiser_analyze(m, 4, 1000));
+    try std.testing.expectEqual(@as(u32, 0), alloyiser_counterexample_count(m));
 
-    const err = {{project}}_last_error();
-    try std.testing.expect(err != null);
+    const als = alloyiser_model_to_als(m) orelse return error.RenderFailed;
+    defer alloyiser_free_string(als);
+    try std.testing.expect(std.mem.indexOf(u8, std.mem.span(als), "sig Node") != null);
 }
 
-test "version" {
-    const ver = {{project}}_version();
-    const ver_str = std.mem.span(ver);
-    try std.testing.expectEqualStrings(VERSION, ver_str);
+test "null handle is rejected" {
+    try std.testing.expectEqual(code(.null_pointer), alloyiser_add_fact(null, "f", "true"));
+    try std.testing.expectEqual(@as(u32, 0), alloyiser_counterexample_count(null));
 }