diff --git a/docs/avm_ports_audit.md b/docs/avm_ports_audit.md
new file mode 100644
index 00000000..51806352
--- /dev/null
+++ b/docs/avm_ports_audit.md
@@ -0,0 +1,97 @@
+# AVM ISA Ports — Cross-Implementation Audit
+
+**Date:** 2026-06-30
+**Reference:** `formal/SilverSight/AVMIsa/Step.lean` (Lean 4)
+**Ports audited:** Rust, Julia, R
+
+## 1. Critical: Integer Division Semantics (ALL PORTS)
+
+**Lean 4 uses `Int.ediv` which rounds toward NEGATIVE INFINITY (floor).**
+All three ports use truncation-toward-zero division.
+
+| Expression | Lean (ediv) | Rust/R/Julia | Impact |
+|-----------|------------|--------------|--------|
+| `(-5 * 65536) / 3` | `-109227` (floor) | `-109226` (trunc) | ❌ Off by 1 |
+| `(-1 * 65536) / 65536` | `-1` | `-1` | ✅ Same |
+| `(5 * 65536) / 3` | `109226` | `109226` | ✅ Same |
+| `(5 * 65536) / -3` | `-109227` | `-109226` | ❌ Off by 1 |
+
+**Fix:** All ports must match Lean's floor division for negative values.
+
+The Q16_16 multiplication `(a * b) / 65536` only differs when `(a*b)` is negative
+and not evenly divisible by 65536 — a 1-LSB error in the fractional part. While
+small, this breaks the determinism contract.
+
+## 2. Rust port (`rust/src/avm/mod.rs`)
+
+| Issue | Severity | Detail |
+|-------|----------|--------|
+| Division semantics | **HIGH** | Uses truncation, not floor |
+| Signed comparison (ltQ16) | **MEDIUM** | Uses raw `<` instead of V6 sign-decomposition (functionally equivalent for the symmetric range `[-2147483647, 2147483647]`, but deviates from spec) |
+| Q16_16 clamp range | **MEDIUM** | Uses `INT32_MIN`/`INT32_MAX` instead of symmetric `[-2147483647, 2147483647]` |
+| Q0_16 clamp range | **MEDIUM** | Uses `[-32768, 32767]` instead of `[-32767, 32767]` |
+| No stack depth limit | **MEDIUM** | Missing `maxStackDepth = 1024` check |
+| No StackOverflow error | **MEDIUM** | Missing error variant |
+| Q0_16 `Not` operator | **LOW** | Using a simplified version; Lean has no Q0_16 Not |
+
+### Good:
+- Tagged union types (faithful to Lean)
+- Result-based error handling
+- Fuel-bounded run loop
+- Proper test coverage
+
+## 3. Julia port (`julia/AVMIsa/avm.jl`)
+
+| Issue | Severity | Detail |
+|-------|----------|--------|
+| Division semantics | **HIGH** | Uses truncation, not floor |
+| Signed comparison (ltQ16) | **MEDIUM** | Uses raw `<` (functionally equivalent for symmetric range) |
+| Q16_16 clamp range | **MEDIUM** | Uses `typemin(Int32)` = `-2147483648` instead of `-2147483647` |
+| Missing Q0_16 support | **HIGH** | Lean has `q0_16` type with saturated add/sub |
+| No stack depth limit | **MEDIUM** | Missing `maxStackDepth = 1024` |
+| No StackOverflow error | **MEDIUM** | Missing error variant |
+| Error handling via exceptions | **LOW** | Uses `error()` instead of Result types — loses functional purity |
+| Instr encoding | **LOW** | Uses flat opcode + arg scheme instead of tagged union; fragile |
+
+### Good:
+- Delegates to `Q16_16.q_mul`/`q_div` for correct Q16_16 arithmetic
+- Fuel-bounded run loop
+
+## 4. R port (`r/AVMIsa/avm.r`)
+
+| Issue | Severity | Detail |
+|-------|----------|--------|
+| Division semantics | **HIGH** | Uses `round()` NOT integer truncation; different from both Lean and truncation |
+| Signed comparison (ltQ16) | **MEDIUM** | Uses raw `<` (functionally equivalent for symmetric range) |
+| Q16_16 clamp range | **MEDIUM** | Uses `-2147483648` instead of `-2147483647` |
+| Multiplication rounding | **MEDIUM** | Uses `round()` not integer division — gives different results |
+| `as.integer()` overflow | **MEDIUM** | Silently produces NA for out-of-range values |
+| Missing Q0_16 support | **HIGH** | Lean has `q0_16` type |
+| No stack depth limit | **MEDIUM** | Missing `maxStackDepth = 1024` |
+| No StackOverflow error | **MEDIUM** | Missing error variant |
+
+### Good:
+- Functional style (pure step function)
+- Fuel-bounded run loop
+- Runtime type checking on primitives
+
+## 5. Summary
+
+| Issue | Rust | Julia | R |
+|-------|------|-------|---|
+| Division = floor (Lean ediv) | ❌ | ❌ | ❌ |
+| Signed comparison (V6) | ❌ | ❌ | ❌ |
+| Symmetric Q16_16 clamp | ❌ | ❌ | ❌ |
+| Q0_16 support | ⚠️ | ❌ | ❌ |
+| Stack depth limit | ❌ | ❌ | ❌ |
+| StackOverflow error | ❌ | ❌ | ❌ |
+
+**No port is fully compliant with the Lean reference.** All three have the same
+three systemic issues: division rounding, comparison algorithm, and clamp range.
+
+The floor-vs-truncation issue is the most dangerous — it's a silent 1-LSB error
+on negative values that will accumulate across multiple operations.
+
+Recommendation: fix the division semantics in all three ports first, then the
+comparison and clamp issues. These are all small patches; the port structure
+itself is sound.