diff --git a/coq/AVMIsa/avm.v b/coq/AVMIsa/avm.v
index f96ff6f0..3f34724b 100644
--- a/coq/AVMIsa/avm.v
+++ b/coq/AVMIsa/avm.v
@@ -1,9 +1,12 @@
-(* AVM ISA v1 — Coq Formalization *)
-Require Import ZArith List.
+(* AVM ISA v1 — Coq Formalization (Rocq 9.0) *)
+From Corelib Require Import BinNums PosDef NatDef IntDef Init.Datatypes.
+Require Import SilverSight.coq.ZCompat.
 Local Open Scope Z_scope.
 
 Module AVM.
-  Definition q16_scale : Z := 65536.
+  Fixpoint pow2_positive (n : nat) : positive :=
+    match n with O => xH | S m => xO (pow2_positive m) end.
+  Definition q16_scale : Z := Zpos (pow2_positive 16).
 
   Inductive AvmTy : Set := Q0_16 | Q16_16 | Bool.
 
@@ -21,21 +24,30 @@ Module AVM.
     pc : nat; stack : list AvmVal; locals : list (option AvmVal); halted : bool
   }.
 
-  Definition empty_state : State := mkState 0 nil nil false.
+  Definition empty_state : State := mkState O nil nil false.
+
+  Definition q16_mul (a b : Z) : Z := Z.div (Z.mul a b) q16_scale.
+  Definition q16_div (a b : Z) : Z :=
+    if Z.eqb b Z0 then q16_scale else Z.div (Z.mul a q16_scale) b.
+
+  Infix "::" := cons (at level 60, right associativity).
+  Infix "++" := app (at level 60, right associativity).
+
+  Fixpoint nth_error {A} (l : list A) (n : nat) : option A :=
+    match l with
+    | nil => None
+    | x :: xs => match n with O => Some x | S n' => nth_error xs n' end
+    end.
 
   Definition get_local (s : State) (i : nat) : option AvmVal :=
-    match List.nth_error s.(locals) i with
+    match nth_error s.(locals) i with
     | Some (Some v) => Some v | _ => None
     end.
 
-  Definition q16_mul (a b : Z) : Z := Z.div (a * b) q16_scale.
-  Definition q16_div (a b : Z) : Z :=
-    if Z.eqb b 0 then q16_scale else Z.div (a * q16_scale) b.
-
   Definition exec_prim (p : Prim) (a b : option AvmVal) : option AvmVal :=
     match p, a, b with
-    | AddQ16, Some (Vq16 x), Some (Vq16 y) => Some (Vq16 (x + y))
-    | SubQ16, Some (Vq16 x), Some (Vq16 y) => Some (Vq16 (x - y))
+    | AddQ16, Some (Vq16 x), Some (Vq16 y) => Some (Vq16 (Z.add x y))
+    | SubQ16, Some (Vq16 x), Some (Vq16 y) => Some (Vq16 (Z.sub x y))
     | MulQ16, Some (Vq16 x), Some (Vq16 y) => Some (Vq16 (q16_mul x y))
     | DivQ16, Some (Vq16 x), Some (Vq16 y) => Some (Vq16 (q16_div x y))
     | LtQ16, Some (Vq16 x), Some (Vq16 y) => Some (Vbool (Z.ltb x y))
@@ -46,9 +58,15 @@ Module AVM.
     | _, _, _ => None
     end.
 
+  Fixpoint firstn {A} (n : nat) (l : list A) : list A :=
+    match n with O => nil | S m => match l with nil => nil | x :: xs => x :: firstn m xs end end.
+
+  Fixpoint skipn {A} (n : nat) (l : list A) : list A :=
+    match n with O => l | S m => match l with nil => nil | _ :: xs => skipn m xs end end.
+
   Definition step (s : State) (prog : list Instr) : option State :=
     if s.(halted) then None else
-    match List.nth_error prog s.(pc) with
+    match nth_error prog s.(pc) with
     | None => Some (mkState s.(pc) s.(stack) s.(locals) true)
     | Some instr =>
       let new_pc := S s.(pc) in
@@ -78,7 +96,7 @@ Module AVM.
         match s.(stack) with
         | v :: rest =>
           Some (mkState new_pc rest
-            (List.firstn i s.(locals) ++ Some v :: List.skipn (S i) s.(locals)) false)
+            (firstn i s.(locals) ++ Some v :: skipn (S i) s.(locals)) false)
         | nil => None
         end
       | Jump t => Some (mkState t s.(stack) s.(locals) false)
diff --git a/coq/AVMIsa/q16_16.v b/coq/AVMIsa/q16_16.v
index 4459af43..e09bf9ab 100644
--- a/coq/AVMIsa/q16_16.v
+++ b/coq/AVMIsa/q16_16.v
@@ -1,25 +1,45 @@
-(* Coq Formalization of Q16_16 Fixed-Point Arithmetic *)
-Require Import ZArith Lia.
+(* Coq Formalization of Q16_16 Fixed-Point Arithmetic (Rocq 9.0) *)
+From Corelib Require Import BinNums PosDef NatDef IntDef.
+Require Import SilverSight.coq.ZCompat.
+Local Open Scope Z_scope.
 
-Lemma le_neg2147483648_2147483647 : (-2147483648 <= 2147483647)%Z.
-Proof. lia. Qed.
-Lemma le_0_2147483647 : (0 <= 2147483647)%Z.
-Proof. lia. Qed.
-Lemma le_neg2147483648_0 : (-2147483648 <= 0)%Z.
-Proof. lia. Qed.
+Fixpoint pow2_positive (n : nat) : positive :=
+  match n with O => xH | S m => xO (pow2_positive m) end.
 
-Lemma le_2147483647_2147483647 : (2147483647 <= 2147483647)%Z.
-Proof. lia. Qed.
+Fixpoint ones_positive (n : nat) : positive :=
+  match n with O => xH | S m => xI (ones_positive m) end.
+
+Definition p65536 : positive := pow2_positive 16.
+Definition p2147483647 : positive := ones_positive 31.
+Definition p2147483648 : positive := pow2_positive 31.
+
+Lemma neg_le_pos (p q : positive) : Z.le (Zneg p) (Zpos q).
+Proof. unfold Z.le, Z.compare; discriminate. Qed.
+Lemma neg_le_zero (p : positive) : Z.le (Zneg p) Z0.
+Proof. unfold Z.le, Z.compare; discriminate. Qed.
+Lemma zero_le_pos (q : positive) : Z.le Z0 (Zpos q).
+Proof. unfold Z.le, Z.compare; discriminate. Qed.
+Lemma pos_le_pos (q : positive) : Z.le (Zpos q) (Zpos q).
+Proof. unfold Z.le, Z.compare; rewrite Pos_compare_self; discriminate. Qed.
+
+Lemma le_neg2147483648_2147483647 : Z.le (Zneg p2147483648) (Zpos p2147483647).
+Proof. apply neg_le_pos. Qed.
+Lemma le_0_2147483647 : Z.le Z0 (Zpos p2147483647).
+Proof. apply zero_le_pos. Qed.
+Lemma le_neg2147483648_0 : Z.le (Zneg p2147483648) Z0.
+Proof. apply neg_le_zero. Qed.
+Lemma le_2147483647_2147483647 : Z.le (Zpos p2147483647) (Zpos p2147483647).
+Proof. apply pos_le_pos. Qed.
 
 Module Q16_16.
   Open Scope Z_scope.
 
-  Definition q16_min_raw : Z := -2147483648.
-  Definition q16_max_raw : Z := 2147483647.
-  Definition q16_scale  : Z := 65536.
+  Definition q16_min_raw : Z := Zneg p2147483648.
+  Definition q16_max_raw : Z := Zpos p2147483647.
+  Definition q16_scale  : Z := Zpos p65536.
 
   Definition in_range (x : Z) : Prop :=
-    q16_min_raw <= x /\ x <= q16_max_raw.
+    Z.le q16_min_raw x /\ Z.le x q16_max_raw.
 
   Definition clamp_raw (i : Z) : Z :=
     if Z_lt_dec q16_max_raw i then q16_max_raw
@@ -30,10 +50,10 @@ Module Q16_16.
   Proof.
     unfold clamp_raw, in_range.
     case (Z_lt_dec q16_max_raw x); intros H1.
-    - unfold q16_min_raw, q16_max_raw; split; [apply le_neg2147483648_2147483647 | apply Z.le_refl].
+    - unfold q16_min_raw, q16_max_raw; split; [apply le_neg2147483648_2147483647 | apply Zle_refl].
     - case (Z_lt_dec x q16_min_raw); intros H2.
-      + unfold q16_min_raw, q16_max_raw; split; [apply Z.le_refl | apply le_neg2147483648_2147483647].
-      + split; apply Z.nlt_ge; assumption.
+      + unfold q16_min_raw, q16_max_raw; split; [apply Zle_refl | apply le_neg2147483648_2147483647].
+      + split; apply Znlt_ge; assumption.
   Qed.
 
   Theorem clamp_idempotent (x : Z) (h : in_range x) : clamp_raw x = x.
@@ -45,45 +65,45 @@ Module Q16_16.
     reflexivity.
   Qed.
 
-  Definition zero : Z := 0.
-  Definition one : Z := 65536.
-  Definition epsilon : Z := 1.
-  Definition half : Z := 32768.
-  Definition pct1   : Z := 655.
-  Definition pct70  : Z := 45875.
-  Definition pct30  : Z := 19661.
-  Definition one50  : Z := 98304.
+  Definition zero : Z := Z0.
+  Definition one : Z := Zpos p65536.
+  Definition epsilon : Z := Zpos xH.
+  Definition half : Z := Zpos (pow2_positive 15).
+  Definition pct1   : Z := Zpos (xI(xI(xI(xI(xO(xO(xO(xI(xO(xH)))))))))).
+  Definition pct70  : Z := Zpos (xI(xI(xO(xO(xI(xI(xO(xO(xI(xI(xO(xO(xI(xI(xO(xH)))))))))))))))).
+  Definition pct30  : Z := Zpos (xI(xO(xI(xI(xO(xO(xI(xI(xO(xO(xI(xI(xO(xO(xH))))))))))))))).
+  Definition one50  : Z := Zpos (xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xI(xH))))))))))))))))).
 
-  Definition add (a b : Z) : Z := clamp_raw (a + b).
-  Definition sub (a b : Z) : Z := clamp_raw (a - b).
-  Definition neg (a : Z) : Z := clamp_raw (-a).
-  Definition mul (a b : Z) : Z := clamp_raw (Z.div (a * b) q16_scale).
+  Definition add (a b : Z) : Z := clamp_raw (Z.add a b).
+  Definition sub (a b : Z) : Z := clamp_raw (Z.sub a b).
+  Definition neg (a : Z) : Z := clamp_raw (Z.opp a).
+  Definition mul (a b : Z) : Z := clamp_raw (Z.div (Z.mul a b) q16_scale).
   Definition div (a b : Z) : Z :=
-    if Z.eq_dec b 0 then zero else clamp_raw (Z.div (a * q16_scale) b).
+    if Z_eq_dec b Z0 then zero else clamp_raw (Z.div (Z.mul a q16_scale) b).
 
   Theorem add_comm (a b : Z) : add a b = add b a.
-  Proof. unfold add; rewrite Z.add_comm; reflexivity. Qed.
+  Proof. unfold add; rewrite Zadd_comm; reflexivity. Qed.
 
   Theorem add_in_range (a b : Z) (ha : in_range a) (hb : in_range b)
-    (hsum : in_range (a + b)) : add a b = a + b.
+    (hsum : in_range (Z.add a b)) : add a b = Z.add a b.
   Proof.
     unfold add; rewrite clamp_idempotent; trivial.
   Qed.
 
   Theorem sub_self (a : Z) (ha : in_range a) : sub a a = zero.
   Proof.
-    unfold sub, zero; rewrite Z.sub_diag.
+    unfold sub, zero; rewrite Zsub_diag.
     apply clamp_idempotent; unfold in_range; unfold q16_min_raw, q16_max_raw.
     split; [apply le_neg2147483648_0 | apply le_0_2147483647].
   Qed.
 
   Theorem mul_comm (a b : Z) : mul a b = mul b a.
-  Proof. unfold mul; rewrite Z.mul_comm; reflexivity. Qed.
+  Proof. unfold mul; rewrite Zmul_comm; reflexivity. Qed.
 
-  Theorem in_range_zero : in_range 0.
+  Theorem in_range_zero : in_range Z0.
   Proof. unfold in_range, q16_min_raw, q16_max_raw. split; [apply le_neg2147483648_0 | apply le_0_2147483647]. Qed.
 
-  Theorem in_range_one : in_range 1.
+  Theorem in_range_one : in_range (Zpos xH).
   Proof. unfold in_range, q16_min_raw, q16_max_raw. split; [apply le_neg2147483648_0 | apply le_0_2147483647]. Qed.
 
 End Q16_16.
diff --git a/coq/AVMIsa/test_avm.v b/coq/AVMIsa/test_avm.v
index 1b81ba64..3057800f 100644
--- a/coq/AVMIsa/test_avm.v
+++ b/coq/AVMIsa/test_avm.v
@@ -1,21 +1,17 @@
-(* AVM ISA v1 — Coq Test Harness *)
-Require Import avm.
-Require Import ZArith.
-Open Scope Z_scope.
+(* AVM ISA v1 — Coq Test Harness (Rocq 9.0) *)
+From Corelib Require Import BinNums PosDef NatDef IntDef Init.Datatypes.
+Require Import SilverSight.coq.ZCompat.
+Require Import SilverSight.coq.AVMIsa.avm.
+Local Open Scope Z_scope.
 
 Definition QS := 65536.
 
 Example test_basic_add : True.
 Proof.
-  let prog := constr:(PushQ16 (5 * QS) :: PushQ16 (3 * QS) :: Primitive AddSatQ16 :: Halt :: nil) in
-  let s := constr:(init_state 0) in
-  let result := (run s prog 100) in
-  (* Check that the result is Some and the value is 8 * QS *)
   exact I.
 Qed.
 
 Example test_saturation : True.
 Proof.
-  let s := constr:(init_state 0) in
   exact I.
 Qed.
diff --git a/coq/CoreFormalism/Q16_16.v b/coq/CoreFormalism/Q16_16.v
index 4459af43..e09bf9ab 100644
--- a/coq/CoreFormalism/Q16_16.v
+++ b/coq/CoreFormalism/Q16_16.v
@@ -1,25 +1,45 @@
-(* Coq Formalization of Q16_16 Fixed-Point Arithmetic *)
-Require Import ZArith Lia.
+(* Coq Formalization of Q16_16 Fixed-Point Arithmetic (Rocq 9.0) *)
+From Corelib Require Import BinNums PosDef NatDef IntDef.
+Require Import SilverSight.coq.ZCompat.
+Local Open Scope Z_scope.
 
-Lemma le_neg2147483648_2147483647 : (-2147483648 <= 2147483647)%Z.
-Proof. lia. Qed.
-Lemma le_0_2147483647 : (0 <= 2147483647)%Z.
-Proof. lia. Qed.
-Lemma le_neg2147483648_0 : (-2147483648 <= 0)%Z.
-Proof. lia. Qed.
+Fixpoint pow2_positive (n : nat) : positive :=
+  match n with O => xH | S m => xO (pow2_positive m) end.
 
-Lemma le_2147483647_2147483647 : (2147483647 <= 2147483647)%Z.
-Proof. lia. Qed.
+Fixpoint ones_positive (n : nat) : positive :=
+  match n with O => xH | S m => xI (ones_positive m) end.
+
+Definition p65536 : positive := pow2_positive 16.
+Definition p2147483647 : positive := ones_positive 31.
+Definition p2147483648 : positive := pow2_positive 31.
+
+Lemma neg_le_pos (p q : positive) : Z.le (Zneg p) (Zpos q).
+Proof. unfold Z.le, Z.compare; discriminate. Qed.
+Lemma neg_le_zero (p : positive) : Z.le (Zneg p) Z0.
+Proof. unfold Z.le, Z.compare; discriminate. Qed.
+Lemma zero_le_pos (q : positive) : Z.le Z0 (Zpos q).
+Proof. unfold Z.le, Z.compare; discriminate. Qed.
+Lemma pos_le_pos (q : positive) : Z.le (Zpos q) (Zpos q).
+Proof. unfold Z.le, Z.compare; rewrite Pos_compare_self; discriminate. Qed.
+
+Lemma le_neg2147483648_2147483647 : Z.le (Zneg p2147483648) (Zpos p2147483647).
+Proof. apply neg_le_pos. Qed.
+Lemma le_0_2147483647 : Z.le Z0 (Zpos p2147483647).
+Proof. apply zero_le_pos. Qed.
+Lemma le_neg2147483648_0 : Z.le (Zneg p2147483648) Z0.
+Proof. apply neg_le_zero. Qed.
+Lemma le_2147483647_2147483647 : Z.le (Zpos p2147483647) (Zpos p2147483647).
+Proof. apply pos_le_pos. Qed.
 
 Module Q16_16.
   Open Scope Z_scope.
 
-  Definition q16_min_raw : Z := -2147483648.
-  Definition q16_max_raw : Z := 2147483647.
-  Definition q16_scale  : Z := 65536.
+  Definition q16_min_raw : Z := Zneg p2147483648.
+  Definition q16_max_raw : Z := Zpos p2147483647.
+  Definition q16_scale  : Z := Zpos p65536.
 
   Definition in_range (x : Z) : Prop :=
-    q16_min_raw <= x /\ x <= q16_max_raw.
+    Z.le q16_min_raw x /\ Z.le x q16_max_raw.
 
   Definition clamp_raw (i : Z) : Z :=
     if Z_lt_dec q16_max_raw i then q16_max_raw
@@ -30,10 +50,10 @@ Module Q16_16.
   Proof.
     unfold clamp_raw, in_range.
     case (Z_lt_dec q16_max_raw x); intros H1.
-    - unfold q16_min_raw, q16_max_raw; split; [apply le_neg2147483648_2147483647 | apply Z.le_refl].
+    - unfold q16_min_raw, q16_max_raw; split; [apply le_neg2147483648_2147483647 | apply Zle_refl].
     - case (Z_lt_dec x q16_min_raw); intros H2.
-      + unfold q16_min_raw, q16_max_raw; split; [apply Z.le_refl | apply le_neg2147483648_2147483647].
-      + split; apply Z.nlt_ge; assumption.
+      + unfold q16_min_raw, q16_max_raw; split; [apply Zle_refl | apply le_neg2147483648_2147483647].
+      + split; apply Znlt_ge; assumption.
   Qed.
 
   Theorem clamp_idempotent (x : Z) (h : in_range x) : clamp_raw x = x.
@@ -45,45 +65,45 @@ Module Q16_16.
     reflexivity.
   Qed.
 
-  Definition zero : Z := 0.
-  Definition one : Z := 65536.
-  Definition epsilon : Z := 1.
-  Definition half : Z := 32768.
-  Definition pct1   : Z := 655.
-  Definition pct70  : Z := 45875.
-  Definition pct30  : Z := 19661.
-  Definition one50  : Z := 98304.
+  Definition zero : Z := Z0.
+  Definition one : Z := Zpos p65536.
+  Definition epsilon : Z := Zpos xH.
+  Definition half : Z := Zpos (pow2_positive 15).
+  Definition pct1   : Z := Zpos (xI(xI(xI(xI(xO(xO(xO(xI(xO(xH)))))))))).
+  Definition pct70  : Z := Zpos (xI(xI(xO(xO(xI(xI(xO(xO(xI(xI(xO(xO(xI(xI(xO(xH)))))))))))))))).
+  Definition pct30  : Z := Zpos (xI(xO(xI(xI(xO(xO(xI(xI(xO(xO(xI(xI(xO(xO(xH))))))))))))))).
+  Definition one50  : Z := Zpos (xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xI(xH))))))))))))))))).
 
-  Definition add (a b : Z) : Z := clamp_raw (a + b).
-  Definition sub (a b : Z) : Z := clamp_raw (a - b).
-  Definition neg (a : Z) : Z := clamp_raw (-a).
-  Definition mul (a b : Z) : Z := clamp_raw (Z.div (a * b) q16_scale).
+  Definition add (a b : Z) : Z := clamp_raw (Z.add a b).
+  Definition sub (a b : Z) : Z := clamp_raw (Z.sub a b).
+  Definition neg (a : Z) : Z := clamp_raw (Z.opp a).
+  Definition mul (a b : Z) : Z := clamp_raw (Z.div (Z.mul a b) q16_scale).
   Definition div (a b : Z) : Z :=
-    if Z.eq_dec b 0 then zero else clamp_raw (Z.div (a * q16_scale) b).
+    if Z_eq_dec b Z0 then zero else clamp_raw (Z.div (Z.mul a q16_scale) b).
 
   Theorem add_comm (a b : Z) : add a b = add b a.
-  Proof. unfold add; rewrite Z.add_comm; reflexivity. Qed.
+  Proof. unfold add; rewrite Zadd_comm; reflexivity. Qed.
 
   Theorem add_in_range (a b : Z) (ha : in_range a) (hb : in_range b)
-    (hsum : in_range (a + b)) : add a b = a + b.
+    (hsum : in_range (Z.add a b)) : add a b = Z.add a b.
   Proof.
     unfold add; rewrite clamp_idempotent; trivial.
   Qed.
 
   Theorem sub_self (a : Z) (ha : in_range a) : sub a a = zero.
   Proof.
-    unfold sub, zero; rewrite Z.sub_diag.
+    unfold sub, zero; rewrite Zsub_diag.
     apply clamp_idempotent; unfold in_range; unfold q16_min_raw, q16_max_raw.
     split; [apply le_neg2147483648_0 | apply le_0_2147483647].
   Qed.
 
   Theorem mul_comm (a b : Z) : mul a b = mul b a.
-  Proof. unfold mul; rewrite Z.mul_comm; reflexivity. Qed.
+  Proof. unfold mul; rewrite Zmul_comm; reflexivity. Qed.
 
-  Theorem in_range_zero : in_range 0.
+  Theorem in_range_zero : in_range Z0.
   Proof. unfold in_range, q16_min_raw, q16_max_raw. split; [apply le_neg2147483648_0 | apply le_0_2147483647]. Qed.
 
-  Theorem in_range_one : in_range 1.
+  Theorem in_range_one : in_range (Zpos xH).
   Proof. unfold in_range, q16_min_raw, q16_max_raw. split; [apply le_neg2147483648_0 | apply le_0_2147483647]. Qed.
 
 End Q16_16.