diff --git a/c/avm.c b/c/avm.c
index 60a8f09a..bd277c6e 100644
--- a/c/avm.c
+++ b/c/avm.c
@@ -177,6 +177,8 @@ int step(State *s, const Instr *prog, int prog_len) {
         if (s->sp < arity) return -4;
         AnyVal b = (arity >= 2) ? s->stack[--s->sp] : (AnyVal){0};
         AnyVal a = s->stack[--s->sp];
+        /* Check division by zero before calling eval_prim */
+        if (p == PRIM_DIV_Q16 && b.val.i == 0) return -8;
         s->stack[s->sp++] = eval_prim(p, a, b);
     } else if (instr.op == OP_HALT) {
         s->halted = true;
diff --git a/lakefile.lean b/lakefile.lean
index f5d19392..c54f3d98 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -41,6 +41,7 @@ lean_lib «SilverSightFormal» where
     `CoreFormalism.HachimojiBridging,
     `CoreFormalism.HachimojiManifoldAxiom,
     `CoreFormalism.ChentsovFinite,
+    `CoreFormalism.HopfFibration,
     `SilverSight.WireFormat,
     `SilverSight.ProductSchema,
     `SilverSight.ProductWireFormat,
diff --git a/octave/AVM.m b/octave/AVM.m
index 505d97ed..a5df1df7 100644
--- a/octave/AVM.m
+++ b/octave/AVM.m
@@ -62,7 +62,10 @@ classdef AVM
 
         function s = init_state(n_locals)
             if nargin < 1; n_locals = 0; end
-            s = struct('pc', int32(0), 'stack', {}, 'locals', cell(n_locals, 1), 'halted', false);
+            s.pc = int32(0);
+            s.stack = {};
+            s.locals = cell(n_locals, 1);
+            s.halted = false;
         end
 
         function r = exec_prim(p, a, b)