diff --git a/.github/workflows/q16-roundtrip.yml b/.github/workflows/q16-roundtrip.yml
index 02726fad..5aaba543 100644
--- a/.github/workflows/q16-roundtrip.yml
+++ b/.github/workflows/q16-roundtrip.yml
@@ -6,6 +6,11 @@ jobs:
     steps:
       - uses: actions/checkout@v4
       - name: Build C library
-        run: make -f CBridge/Makefile
-      - name: Run roundtrip test
-        run: python3 Tests/q16_roundtrip_test.py
\ No newline at end of file
+        run: gcc -shared -fPIC -O2 -o c/libq16.so c/q16_canonical.c
+      - name: Build and run roundtrip
+        run: |
+          lake build q16-roundtrip
+          lake exe q16-roundtrip 2>/dev/null | python3 -c 'import json,sys; d=json.load(sys.stdin); assert d["ok"], f"{d[\"failed\"]} failures"; print(f"OK: {d[\"passed\"]}/{d[\"total\"]} passed (0 failed)")'
+      - name: Verify C/Lean agreement
+        run: |
+          lake exe q16-roundtrip 2>/dev/null | python3 -c 'import json,sys; d=json.load(sys.stdin); print(f"C/Lean roundtrip: {d[\"passed\"]}/{d[\"total\"]} consistent")'