diff --git a/crates/console/prometeu-vm/src/virtual_machine.rs b/crates/console/prometeu-vm/src/virtual_machine.rs
index 7e47f499..5c7e5199 100644
--- a/crates/console/prometeu-vm/src/virtual_machine.rs
+++ b/crates/console/prometeu-vm/src/virtual_machine.rs
@@ -92,6 +92,11 @@ pub struct VirtualMachine {
     pub halted: bool,
     /// Set of ROM addresses used for software breakpoints in the debugger.
     pub breakpoints: std::collections::HashSet<usize>,
+    /// GC: number of newly allocated live objects threshold to trigger a collection at safepoint.
+    /// The GC only runs at safepoints (e.g., FRAME_SYNC). 0 disables automatic GC.
+    pub gc_alloc_threshold: usize,
+    /// GC: snapshot of live objects count after the last collection (or VM init).
+    last_gc_live_count: usize,
 }
 
 
@@ -120,6 +125,8 @@ impl VirtualMachine {
             cycles: 0,
             halted: false,
             breakpoints: std::collections::HashSet::new(),
+            gc_alloc_threshold: 1024, // conservative default; tests may override
+            last_gc_live_count: 0,
         }
     }
 
@@ -140,6 +147,7 @@ impl VirtualMachine {
         self.heap = Heap::new();
         self.cycles = 0;
         self.halted = true; // execution is impossible until a successful load
+        self.last_gc_live_count = 0;
 
         // Only recognized format is loadable: PBS v0 industrial format
         let program = if program_bytes.starts_with(b"PBS\0") {
@@ -967,6 +975,30 @@ impl VirtualMachine {
             OpCode::FrameSync => {
                 // Marks the logical end of a frame: consume cycles and signal to the driver
                 self.cycles += OpCode::FrameSync.cycles();
+
+                // GC Safepoint: only at FRAME_SYNC
+                if self.gc_alloc_threshold > 0 {
+                    let live_now = self.heap.len();
+                    let since_last = live_now.saturating_sub(self.last_gc_live_count);
+                    if since_last >= self.gc_alloc_threshold {
+                        // Collect GC roots from VM state
+                        struct CollectRoots(Vec<prometeu_bytecode::HeapRef>);
+                        impl crate::roots::RootVisitor for CollectRoots {
+                            fn visit_heap_ref(&mut self, r: prometeu_bytecode::HeapRef) {
+                                self.0.push(r);
+                            }
+                        }
+                        let mut collector = CollectRoots(Vec::new());
+                        self.visit_roots(&mut collector);
+
+                        // Run mark-sweep
+                        self.heap.mark_from_roots(collector.0);
+                        self.heap.sweep();
+                        // Update baseline for next cycles
+                        self.last_gc_live_count = self.heap.len();
+                    }
+                }
+
                 return Err(LogicalFrameEndingReason::FrameSync);
             }
         }
@@ -2461,4 +2493,82 @@ mod tests {
             _ => panic!("Expected Trap, got {:?}", report.reason),
         }
     }
+
+    #[test]
+    fn test_gc_triggers_only_at_frame_sync() {
+        use crate::object::ObjectKind;
+
+        // ROM: NOP; FRAME_SYNC; HALT
+        let mut rom = Vec::new();
+        rom.extend_from_slice(&(OpCode::Nop as u16).to_le_bytes());
+        rom.extend_from_slice(&(OpCode::FrameSync as u16).to_le_bytes());
+        rom.extend_from_slice(&(OpCode::Halt as u16).to_le_bytes());
+
+        let mut vm = new_test_vm(rom.clone(), vec![]);
+        vm.program.functions = std::sync::Arc::from(vec![prometeu_bytecode::FunctionMeta {
+            code_offset: 0,
+            code_len: rom.len() as u32,
+            ..Default::default()
+        }]);
+
+        // Set a very low threshold to trigger GC as soon as we hit FRAME_SYNC
+        vm.gc_alloc_threshold = 1;
+
+        // Allocate an unreachable object (no roots referencing it)
+        let _orphan = vm.heap.allocate_object(ObjectKind::Bytes, &[1, 2, 3]);
+        assert_eq!(vm.heap.len(), 1);
+
+        let mut native = MockNative;
+        let mut ctx = HostContext::new(None);
+
+        // Step 1: NOP — should not run GC
+        vm.step(&mut native, &mut ctx).unwrap();
+        assert_eq!(vm.heap.len(), 1, "GC must not run except at safepoints");
+
+        // Step 2: FRAME_SYNC — GC should run and reclaim the unreachable object
+        match vm.step(&mut native, &mut ctx) {
+            Err(LogicalFrameEndingReason::FrameSync) => {}
+            other => panic!("Expected FrameSync, got {:?}", other),
+        }
+        assert_eq!(vm.heap.len(), 0, "Unreachable object must be reclaimed at FRAME_SYNC");
+    }
+
+    #[test]
+    fn test_gc_keeps_roots_and_collects_unreachable_at_frame_sync() {
+        use crate::object::ObjectKind;
+
+        // ROM: FRAME_SYNC; HALT
+        let mut rom = Vec::new();
+        rom.extend_from_slice(&(OpCode::FrameSync as u16).to_le_bytes());
+        rom.extend_from_slice(&(OpCode::Halt as u16).to_le_bytes());
+
+        let mut vm = new_test_vm(rom.clone(), vec![]);
+        vm.program.functions = std::sync::Arc::from(vec![prometeu_bytecode::FunctionMeta {
+            code_offset: 0,
+            code_len: rom.len() as u32,
+            ..Default::default()
+        }]);
+
+        vm.gc_alloc_threshold = 1;
+
+        // Allocate two objects; make one a root by placing it on the operand stack
+        let rooted = vm.heap.allocate_object(ObjectKind::Bytes, &[9, 9]);
+        let unreachable = vm.heap.allocate_object(ObjectKind::Bytes, &[8, 8, 8]);
+        assert_eq!(vm.heap.len(), 2);
+        vm.operand_stack.push(Value::HeapRef(rooted));
+
+        let mut native = MockNative;
+        let mut ctx = HostContext::new(None);
+
+        // Execute FRAME_SYNC: should trigger GC
+        match vm.step(&mut native, &mut ctx) {
+            Err(LogicalFrameEndingReason::FrameSync) => {}
+            other => panic!("Expected FrameSync, got {:?}", other),
+        }
+
+        // Rooted must survive; unreachable must be collected
+        assert_eq!(vm.heap.len(), 1);
+        assert!(vm.heap.is_valid(rooted));
+        assert!(!vm.heap.is_valid(unreachable));
+    }
 }
diff --git a/files/TODOs.md b/files/TODOs.md
index f1d35b15..b324b30d 100644
--- a/files/TODOs.md
+++ b/files/TODOs.md
@@ -1,50 +1,3 @@
-# PR-3.7 — Integrate GC Cycle at Safepoint (`FRAME_SYNC`)
-
-### Briefing
-
-The GC must only run at safepoints. This PR connects the mark-sweep collector to the VM’s safepoint logic, primarily at `FRAME_SYNC`.
-
-### Target
-
-* Trigger GC cycles only at safepoints.
-* Keep execution deterministic.
-
-### Work items
-
-* Identify safepoint handling code in the VM.
-* Add logic:
-
-  * If allocation threshold exceeded, run GC at `FRAME_SYNC`.
-* Ensure GC does not run in arbitrary instruction contexts.
-
-### Acceptance checklist
-
-* [ ] GC runs only at safepoints.
-* [ ] No GC during arbitrary instruction execution.
-* [ ] VM remains deterministic.
-* [ ] `cargo test` passes.
-
-### Tests
-
-* Add a test where allocations trigger GC only at `FRAME_SYNC`.
-
-### Junie instructions
-
-**You MAY:**
-
-* Hook GC invocation into safepoint handling.
-
-**You MUST NOT:**
-
-* Trigger GC at random points.
-* Add background or concurrent GC.
-
-**If unclear:**
-
-* Ask before modifying safepoint semantics.
-
----
-
 # PR-3.8 — GC Smoke and Stress Tests
 
 ### Briefing
@@ -89,3 +42,357 @@ We need confidence that the GC behaves correctly under simple and stressed condi
 **If unclear:**
 
 * Ask before changing test scenarios.
+# PR-4.1 — Define Canonical Stack Effect Table for Core ISA
+
+### Briefing
+
+The verifier must rely on a single canonical definition of stack effects for every opcode. This PR introduces the formal stack effect table for the new core ISA.
+
+### Target
+
+* Provide a single authoritative stack effect definition per opcode.
+* Ensure verifier and tooling use the same source of truth.
+
+### Work items
+
+* Introduce a stack effect table or equivalent structure:
+
+  * Input slot count.
+  * Output slot count.
+* Attach stack effect metadata to each opcode.
+* Ensure the table is used by the verifier entry points.
+* Document stack effects in code comments (English).
+
+### Acceptance checklist
+
+* [ ] Every opcode has a defined stack effect.
+* [ ] Verifier uses the canonical table.
+* [ ] No duplicated or ad-hoc stack effect logic remains.
+* [ ] `cargo test` passes.
+
+### Tests
+
+* Add unit test ensuring all opcodes have stack effects defined.
+
+### Junie instructions
+
+**You MAY:**
+
+* Introduce new metadata tables for opcodes.
+* Refactor verifier code to use the canonical table.
+
+**You MUST NOT:**
+
+* Change opcode semantics.
+* Introduce new instructions.
+
+**If unclear:**
+
+* Ask before assigning stack effects.
+
+---
+
+# PR-4.2 — Basic Stack Safety Verification (Underflow/Overflow)
+
+### Briefing
+
+The verifier must ensure the stack never underflows or exceeds defined limits during execution.
+
+### Target
+
+* Implement stack safety checks across the control-flow graph.
+
+### Work items
+
+* Simulate stack depth across instructions.
+* Detect:
+
+  * Stack underflow.
+  * Stack overflow beyond declared limits.
+* Emit appropriate verifier errors.
+
+### Acceptance checklist
+
+* [ ] Underflow cases are rejected.
+* [ ] Overflow cases are rejected.
+* [ ] Valid programs pass.
+* [ ] `cargo test` passes.
+
+### Tests
+
+* Add tests:
+
+  * Program with underflow → verifier error.
+  * Program exceeding stack limit → verifier error.
+  * Valid program → passes.
+
+### Junie instructions
+
+**You MAY:**
+
+* Add stack depth simulation.
+* Introduce verifier error types.
+
+**You MUST NOT:**
+
+* Change runtime stack implementation.
+* Introduce dynamic stack resizing.
+
+**If unclear:**
+
+* Ask before choosing stack limit rules.
+
+---
+
+# PR-4.3 — Control Flow and Jump Target Verification
+
+### Briefing
+
+The verifier must ensure all control flow transfers are valid and do not jump into the middle of instructions or outside function boundaries.
+
+### Target
+
+* Validate all jump targets.
+* Reject invalid or unsafe control flow.
+
+### Work items
+
+* Use canonical layout utilities to identify instruction boundaries.
+* Verify:
+
+  * Jump targets land on valid instruction boundaries.
+  * Targets are within the function range.
+* Reject invalid targets with a verifier error.
+
+### Acceptance checklist
+
+* [ ] Invalid jump targets are rejected.
+* [ ] Valid programs pass verification.
+* [ ] No reliance on runtime traps for these cases.
+* [ ] `cargo test` passes.
+
+### Tests
+
+* Add tests:
+
+  * Jump to middle of instruction → verifier error.
+  * Jump outside function → verifier error.
+  * Valid jump → passes.
+
+### Junie instructions
+
+**You MAY:**
+
+* Reuse layout utilities for boundary checks.
+* Add verifier error cases.
+
+**You MUST NOT:**
+
+* Modify instruction encoding.
+* Introduce new trap codes.
+
+**If unclear:**
+
+* Ask before defining jump rules.
+
+---
+
+# PR-4.4 — Function Boundary and Terminator Verification
+
+### Briefing
+
+Functions must follow canonical entry and exit rules. The verifier must enforce valid terminators and boundaries.
+
+### Target
+
+* Ensure functions start and end correctly.
+* Ensure terminator instructions are valid.
+
+### Work items
+
+* Verify function entry points are valid instruction boundaries.
+* Verify function exit instructions:
+
+  * Proper `RET` usage.
+  * Proper `FRAME_SYNC` placement (as per spec).
+* Reject functions without valid termination.
+
+### Acceptance checklist
+
+* [ ] All functions have valid entry and exit.
+* [ ] Invalid termination is rejected.
+* [ ] `cargo test` passes.
+
+### Tests
+
+* Add tests:
+
+  * Function without terminator → verifier error.
+  * Properly terminated function → passes.
+
+### Junie instructions
+
+**You MAY:**
+
+* Add boundary validation logic.
+
+**You MUST NOT:**
+
+* Redefine function semantics.
+* Change terminator opcode behavior.
+
+**If unclear:**
+
+* Ask before enforcing termination rules.
+
+---
+
+# PR-4.5 — Multi-Return (`ret_slots`) Verification
+
+### Briefing
+
+The new ABI supports multi-return via `ret_slots`. The verifier must ensure the stack shape matches the declared return slot count.
+
+### Target
+
+* Validate return slot counts at call and return sites.
+
+### Work items
+
+* For each function:
+
+  * Read declared `ret_slots`.
+* At `RET`:
+
+  * Ensure stack contains exactly the required number of slots.
+* At call sites:
+
+  * Ensure caller expects correct number of return slots.
+
+### Acceptance checklist
+
+* [ ] Mismatched return slot counts are rejected.
+* [ ] Correct programs pass.
+* [ ] `cargo test` passes.
+
+### Tests
+
+* Add tests:
+
+  * Too few return slots → verifier error.
+  * Too many return slots → verifier error.
+  * Correct return slots → passes.
+
+### Junie instructions
+
+**You MAY:**
+
+* Use function metadata to validate returns.
+
+**You MUST NOT:**
+
+* Change calling convention semantics.
+* Modify function metadata layout.
+
+**If unclear:**
+
+* Ask before implementing slot rules.
+
+---
+
+# PR-4.6 — Verifier Error Model Consolidation
+
+### Briefing
+
+Verifier errors must be deterministic, structured, and clearly separated from runtime traps.
+
+### Target
+
+* Introduce a coherent verifier error model.
+
+### Work items
+
+* Define a `VerifierError` enum covering:
+
+  * Stack underflow.
+  * Stack overflow.
+  * Invalid jump target.
+  * Invalid function boundary.
+  * Return slot mismatch.
+* Ensure verifier returns structured errors.
+* Update tests to expect structured errors.
+
+### Acceptance checklist
+
+* [ ] Verifier errors are structured and deterministic.
+* [ ] No reliance on runtime traps for verifier failures.
+* [ ] `cargo test` passes.
+
+### Tests
+
+* Update existing tests to assert specific verifier errors.
+
+### Junie instructions
+
+**You MAY:**
+
+* Introduce a new verifier error enum.
+* Refactor error returns.
+
+**You MUST NOT:**
+
+* Map verifier errors to runtime traps.
+* Change runtime trap behavior.
+
+**If unclear:**
+
+* Ask before merging or renaming error categories.
+
+---
+
+# PR-4.7 — Verifier Golden Test Suite
+
+### Briefing
+
+We need a stable suite of valid and invalid bytecode samples to ensure verifier correctness over time.
+
+### Target
+
+* Introduce golden tests for the verifier.
+
+### Work items
+
+* Add a set of small bytecode samples:
+
+  * Valid programs.
+  * Invalid programs for each verifier error.
+* Implement golden tests asserting:
+
+  * Successful verification.
+  * Specific error kinds for invalid programs.
+
+### Acceptance checklist
+
+* [ ] Golden tests exist for all verifier error categories.
+* [ ] Tests are deterministic.
+* [ ] `cargo test` passes.
+
+### Tests
+
+* New golden tests only.
+
+### Junie instructions
+
+**You MAY:**
+
+* Add deterministic golden tests.
+
+**You MUST NOT:**
+
+* Modify verifier logic to fit tests without understanding the cause.
+* Introduce random or timing-based tests.
+
+**If unclear:**
+
+* Ask before changing test expectations.
+