diff --git a/.github/actions/compile-witness-generator/action.yml b/.github/actions/compile-witness-generator/action.yml
index 16a5866..c3f3d15 100644
--- a/.github/actions/compile-witness-generator/action.yml
+++ b/.github/actions/compile-witness-generator/action.yml
@@ -104,6 +104,13 @@ runs:
         if [ "$OS" = "macos" ]; then SED_I="sed -i ''"; fi
         $SED_I ':a;N;$!ba;s/\n}\n\n*$/\n  return 0;\n}/' "${CIRCUIT_CPP_PATH}/main.cpp"
 
+    - name: Install llvm-objcopy (macOS)
+      if: ${{ inputs.os == 'macos' }}
+      shell: bash
+      run: |
+        brew install llvm
+        echo "$(brew --prefix llvm)/bin" >> "$GITHUB_PATH"
+
     # TODO: Instead of insertion, make a fork that includes the appropriate patch (or the actual fix)
     - name: Patch MacOS GMP
       shell: bash
diff --git a/.github/resources/witness-generator/Makefile b/.github/resources/witness-generator/Makefile
index 227f451..4727b49 100644
--- a/.github/resources/witness-generator/Makefile
+++ b/.github/resources/witness-generator/Makefile
@@ -59,25 +59,21 @@ windows-lib: $(LIB)
 # section" errors that GNU objcopy causes. On Windows/COFF: GNU objcopy suffices
 # because COFF COMDAT is per-section (not group-based) and is already deduplicated
 # automatically by the linker — the ELF GRP_COMDAT problem does not apply.
+# On macOS/Mach-O: llvm-objcopy (from brew install llvm) is used — it supports
+# --keep-global-symbol for Mach-O since LLVM 12.
 PUBLIC_SYMS := $(PROJECT)_generate_witness $(PROJECT)_generate_witness_from_files
 LOCAL_OBJ   := $(PROJECT)_local.o
 OBJCOPY     := $(if $(filter windows,$(OS)),objcopy,llvm-objcopy)
 
-UNAME := $(shell uname -s)
-
 # ---- Rules ----
 $(BIN): $(COMMON_OBJS)
 	$(CXX) $(LDFLAGS) $^ $(LDLIBS) -o $@
 
 $(LIB): $(LIB_OBJS)
-ifeq ($(UNAME),Darwin)
-	ar rcs $@ $^  # macOS: two-level namespace, conflicts don't arise
-else
 	ld -r -o $(LOCAL_OBJ) $(filter-out fr.o,$^)
 	$(OBJCOPY) $(foreach s,$(PUBLIC_SYMS),--keep-global-symbol=$(s)) $(LOCAL_OBJ)
 	ar rcs $@ fr.o $(LOCAL_OBJ)
 	rm $(LOCAL_OBJ)
-endif
 
 %.o: %.cpp $(DEPS_HPP)
 	$(CXX) $(CXXFLAGS) -c $< -o $@
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index e0d5c5d..d2d4c02 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -6,7 +6,7 @@
 
 - [Rust](https://rustup.rs/) — the pinned toolchain version is in `rust-toolchain.toml` and will be installed automatically by `rustup`.
 - [pre-commit](https://pre-commit.com/) — used to run formatting, linting, and audit checks before each commit.
-- `llvm-objcopy` — required to build circuit static libraries (symbol isolation) on Linux. Install via `sudo apt install -y llvm`. On Windows (MSYS2), GNU `objcopy` from `mingw-w64-x86_64-toolchain` is used instead (no extra install needed). On macOS, symbol isolation is skipped entirely, so no objcopy tool is required.
+- `llvm-objcopy` — required to build circuit static libraries (symbol isolation).
 
 ### Installing the Pre-Commit Hooks
 
@@ -58,13 +58,12 @@ page, which results in a **SIGSEGV**.
 
 ### The Fix
 
-The Makefile's `$(LIB)` rule uses a two-step process on Linux and Windows to localize all circuit-specific code before
-archiving:
+The Makefile's `$(LIB)` rule uses a two-step process to localize all circuit-specific code before archiving:
 
 1. **Partial link** (`ld -r`): merges all circuit-specific `.o` files — everything except `fr.o` (pure field
 arithmetic, no circuit-specific calls) — into a single relocatable object. No symbols are resolved yet; this is
 consolidation only.
-2. **Symbol localization** (`llvm-objcopy --keep-global-symbol` on Linux, `objcopy --keep-global-symbol` on Windows): demotes every global symbol to local *except* the
+2. **Symbol localization** (`llvm-objcopy --keep-global-symbol` / `objcopy --keep-global-symbol`): demotes every global symbol to local *except* the
 circuit's two public FFI entry points (`$(PROJECT)_generate_witness` and `$(PROJECT)_generate_witness_from_files`).
 Local symbols are invisible to the final linker, so each archive retains a private copy of every internal symbol — no
 conflict is possible regardless of how many circuits are linked together.
@@ -78,8 +77,8 @@ regular non-COMDAT sections that are simply kept as-is rather than deduplicated.
 `fr.o` is excluded from the merge because it contains only field arithmetic (`Fr_*`) with no circuit-specific calls.
 It is safe to deduplicate across circuits — the linker picks one copy, which is correct since the code is identical.
 
-On macOS, localization is skipped. macOS uses a two-level namespace by default, meaning symbols are qualified by which
-library they come from, so the conflict does not arise.
+On macOS/Mach-O, `llvm-objcopy` (from `brew install llvm`) is used — it supports `--keep-global-symbol` for
+Mach-O since LLVM 12. It is not available in Xcode's toolchain and must be installed separately.
 
 On Windows, GNU `objcopy` (from MinGW binutils) is used instead of `llvm-objcopy`. `llvm-objcopy --keep-global-symbol`
 is not supported for COFF objects, but GNU `objcopy --keep-global-symbol` works correctly on COFF — it maps the local