diff --git a/.github/workflows/clean-circuits.yml b/.github/workflows/clean-circuits.yml
new file mode 100644
index 000000000..12a53afe8
--- /dev/null
+++ b/.github/workflows/clean-circuits.yml
@@ -0,0 +1,49 @@
+name: Clean circuits
+
+on:
+  pull_request:
+    paths:
+      - verification/circuits/**
+      - crates/flock/src/clean.rs
+      - .github/workflows/clean-circuits.yml
+      - rustfmt.toml
+  push:
+    branches: [riscv-exploration, 'kw/clean-circuits-*']
+    paths:
+      - verification/circuits/**
+      - crates/flock/src/clean.rs
+      - .github/workflows/clean-circuits.yml
+      - rustfmt.toml
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  export:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          toolchain: 1.97.0
+          components: rustfmt
+      - uses: leanprover/lean-action@v1
+        with:
+          lake-package-directory: verification/circuits
+          build: 'false'
+          test: 'false'
+          lint: 'false'
+          use-mathlib-cache: 'false'
+      - name: Check source, lowering, artifact, and theorem axioms
+        working-directory: verification/circuits
+        run: |
+          lake exe cache get Mathlib.Tactic
+          lake build
+          lake env lean Audit.lean
+          lake env leanchecker LeanVMCircuits
+      - name: Check deterministic production export
+        working-directory: verification/circuits
+        run: |
+          lake env lean --run Generate.lean /tmp/clean-generated.rs
+          diff -u ../../crates/flock/src/clean.rs /tmp/clean-generated.rs
diff --git a/.gitignore b/.gitignore
index 69de9f663..0f635aba2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,3 +3,4 @@ target
 __pycache__/
 formal/
 conformance/act4/elf/
+verification/circuits/.lake/
diff --git a/README.md b/README.md
index 55e463cfa..82e065e3f 100644
--- a/README.md
+++ b/README.md
@@ -32,6 +32,8 @@ leanVM is designed for security:
 
 **warning**: Formal verification is [in progress](https://github.com/Verified-zkEVM/leanerVM). leanVM is not (yet) production ready.
 
+The production 64-bit wrapping address adder is authored and proved in [Clean](./verification/circuits/README.md), then exported as checked-in Rust gates. Real load and store circuits consume that artifact. Its proofs cover arbitrary-witness Boolean constraint soundness and honest completeness; the Rust interpretation and the separate cryptographic composition retain the trust boundaries documented there.
+
 ## work in progress
 
 Expect leanVM to change significantly:
diff --git a/crates/flock/src/clean.rs b/crates/flock/src/clean.rs
new file mode 100644
index 000000000..71a1d5783
--- /dev/null
+++ b/crates/flock/src/clean.rs
@@ -0,0 +1,829 @@
+// Generated by verification/circuits/Generate.lean from checked Flock artifacts. Do not edit.
+//! Clean-authored GF(2) circuits consumed by production instruction classes.
+
+use crate::circuit::{Builder, Wire};
+
+/// The checked wrapping_add64 artifact, least-significant-bit products first.
+pub fn wrapping_add64(c: &mut Builder, x: &[Wire; 64], y: &[Wire; 64]) -> [Wire; 64] {
+    let w0 = c.xor(x[0], Wire::ZERO);
+    let w1 = c.xor(y[0], Wire::ZERO);
+    let w2 = c.and(w0, w1);
+    let w3 = c.xor(w2, Wire::ZERO);
+    let w4 = c.xor(x[1], w3);
+    let w5 = c.xor(y[1], w3);
+    let w6 = c.and(w4, w5);
+    let w7 = c.xor(w6, w3);
+    let w8 = c.xor(x[2], w7);
+    let w9 = c.xor(y[2], w7);
+    let w10 = c.and(w8, w9);
+    let w11 = c.xor(w10, w7);
+    let w12 = c.xor(x[3], w11);
+    let w13 = c.xor(y[3], w11);
+    let w14 = c.and(w12, w13);
+    let w15 = c.xor(w14, w11);
+    let w16 = c.xor(x[4], w15);
+    let w17 = c.xor(y[4], w15);
+    let w18 = c.and(w16, w17);
+    let w19 = c.xor(w18, w15);
+    let w20 = c.xor(x[5], w19);
+    let w21 = c.xor(y[5], w19);
+    let w22 = c.and(w20, w21);
+    let w23 = c.xor(w22, w19);
+    let w24 = c.xor(x[6], w23);
+    let w25 = c.xor(y[6], w23);
+    let w26 = c.and(w24, w25);
+    let w27 = c.xor(w26, w23);
+    let w28 = c.xor(x[7], w27);
+    let w29 = c.xor(y[7], w27);
+    let w30 = c.and(w28, w29);
+    let w31 = c.xor(w30, w27);
+    let w32 = c.xor(x[8], w31);
+    let w33 = c.xor(y[8], w31);
+    let w34 = c.and(w32, w33);
+    let w35 = c.xor(w34, w31);
+    let w36 = c.xor(x[9], w35);
+    let w37 = c.xor(y[9], w35);
+    let w38 = c.and(w36, w37);
+    let w39 = c.xor(w38, w35);
+    let w40 = c.xor(x[10], w39);
+    let w41 = c.xor(y[10], w39);
+    let w42 = c.and(w40, w41);
+    let w43 = c.xor(w42, w39);
+    let w44 = c.xor(x[11], w43);
+    let w45 = c.xor(y[11], w43);
+    let w46 = c.and(w44, w45);
+    let w47 = c.xor(w46, w43);
+    let w48 = c.xor(x[12], w47);
+    let w49 = c.xor(y[12], w47);
+    let w50 = c.and(w48, w49);
+    let w51 = c.xor(w50, w47);
+    let w52 = c.xor(x[13], w51);
+    let w53 = c.xor(y[13], w51);
+    let w54 = c.and(w52, w53);
+    let w55 = c.xor(w54, w51);
+    let w56 = c.xor(x[14], w55);
+    let w57 = c.xor(y[14], w55);
+    let w58 = c.and(w56, w57);
+    let w59 = c.xor(w58, w55);
+    let w60 = c.xor(x[15], w59);
+    let w61 = c.xor(y[15], w59);
+    let w62 = c.and(w60, w61);
+    let w63 = c.xor(w62, w59);
+    let w64 = c.xor(x[16], w63);
+    let w65 = c.xor(y[16], w63);
+    let w66 = c.and(w64, w65);
+    let w67 = c.xor(w66, w63);
+    let w68 = c.xor(x[17], w67);
+    let w69 = c.xor(y[17], w67);
+    let w70 = c.and(w68, w69);
+    let w71 = c.xor(w70, w67);
+    let w72 = c.xor(x[18], w71);
+    let w73 = c.xor(y[18], w71);
+    let w74 = c.and(w72, w73);
+    let w75 = c.xor(w74, w71);
+    let w76 = c.xor(x[19], w75);
+    let w77 = c.xor(y[19], w75);
+    let w78 = c.and(w76, w77);
+    let w79 = c.xor(w78, w75);
+    let w80 = c.xor(x[20], w79);
+    let w81 = c.xor(y[20], w79);
+    let w82 = c.and(w80, w81);
+    let w83 = c.xor(w82, w79);
+    let w84 = c.xor(x[21], w83);
+    let w85 = c.xor(y[21], w83);
+    let w86 = c.and(w84, w85);
+    let w87 = c.xor(w86, w83);
+    let w88 = c.xor(x[22], w87);
+    let w89 = c.xor(y[22], w87);
+    let w90 = c.and(w88, w89);
+    let w91 = c.xor(w90, w87);
+    let w92 = c.xor(x[23], w91);
+    let w93 = c.xor(y[23], w91);
+    let w94 = c.and(w92, w93);
+    let w95 = c.xor(w94, w91);
+    let w96 = c.xor(x[24], w95);
+    let w97 = c.xor(y[24], w95);
+    let w98 = c.and(w96, w97);
+    let w99 = c.xor(w98, w95);
+    let w100 = c.xor(x[25], w99);
+    let w101 = c.xor(y[25], w99);
+    let w102 = c.and(w100, w101);
+    let w103 = c.xor(w102, w99);
+    let w104 = c.xor(x[26], w103);
+    let w105 = c.xor(y[26], w103);
+    let w106 = c.and(w104, w105);
+    let w107 = c.xor(w106, w103);
+    let w108 = c.xor(x[27], w107);
+    let w109 = c.xor(y[27], w107);
+    let w110 = c.and(w108, w109);
+    let w111 = c.xor(w110, w107);
+    let w112 = c.xor(x[28], w111);
+    let w113 = c.xor(y[28], w111);
+    let w114 = c.and(w112, w113);
+    let w115 = c.xor(w114, w111);
+    let w116 = c.xor(x[29], w115);
+    let w117 = c.xor(y[29], w115);
+    let w118 = c.and(w116, w117);
+    let w119 = c.xor(w118, w115);
+    let w120 = c.xor(x[30], w119);
+    let w121 = c.xor(y[30], w119);
+    let w122 = c.and(w120, w121);
+    let w123 = c.xor(w122, w119);
+    let w124 = c.xor(x[31], w123);
+    let w125 = c.xor(y[31], w123);
+    let w126 = c.and(w124, w125);
+    let w127 = c.xor(w126, w123);
+    let w128 = c.xor(x[32], w127);
+    let w129 = c.xor(y[32], w127);
+    let w130 = c.and(w128, w129);
+    let w131 = c.xor(w130, w127);
+    let w132 = c.xor(x[33], w131);
+    let w133 = c.xor(y[33], w131);
+    let w134 = c.and(w132, w133);
+    let w135 = c.xor(w134, w131);
+    let w136 = c.xor(x[34], w135);
+    let w137 = c.xor(y[34], w135);
+    let w138 = c.and(w136, w137);
+    let w139 = c.xor(w138, w135);
+    let w140 = c.xor(x[35], w139);
+    let w141 = c.xor(y[35], w139);
+    let w142 = c.and(w140, w141);
+    let w143 = c.xor(w142, w139);
+    let w144 = c.xor(x[36], w143);
+    let w145 = c.xor(y[36], w143);
+    let w146 = c.and(w144, w145);
+    let w147 = c.xor(w146, w143);
+    let w148 = c.xor(x[37], w147);
+    let w149 = c.xor(y[37], w147);
+    let w150 = c.and(w148, w149);
+    let w151 = c.xor(w150, w147);
+    let w152 = c.xor(x[38], w151);
+    let w153 = c.xor(y[38], w151);
+    let w154 = c.and(w152, w153);
+    let w155 = c.xor(w154, w151);
+    let w156 = c.xor(x[39], w155);
+    let w157 = c.xor(y[39], w155);
+    let w158 = c.and(w156, w157);
+    let w159 = c.xor(w158, w155);
+    let w160 = c.xor(x[40], w159);
+    let w161 = c.xor(y[40], w159);
+    let w162 = c.and(w160, w161);
+    let w163 = c.xor(w162, w159);
+    let w164 = c.xor(x[41], w163);
+    let w165 = c.xor(y[41], w163);
+    let w166 = c.and(w164, w165);
+    let w167 = c.xor(w166, w163);
+    let w168 = c.xor(x[42], w167);
+    let w169 = c.xor(y[42], w167);
+    let w170 = c.and(w168, w169);
+    let w171 = c.xor(w170, w167);
+    let w172 = c.xor(x[43], w171);
+    let w173 = c.xor(y[43], w171);
+    let w174 = c.and(w172, w173);
+    let w175 = c.xor(w174, w171);
+    let w176 = c.xor(x[44], w175);
+    let w177 = c.xor(y[44], w175);
+    let w178 = c.and(w176, w177);
+    let w179 = c.xor(w178, w175);
+    let w180 = c.xor(x[45], w179);
+    let w181 = c.xor(y[45], w179);
+    let w182 = c.and(w180, w181);
+    let w183 = c.xor(w182, w179);
+    let w184 = c.xor(x[46], w183);
+    let w185 = c.xor(y[46], w183);
+    let w186 = c.and(w184, w185);
+    let w187 = c.xor(w186, w183);
+    let w188 = c.xor(x[47], w187);
+    let w189 = c.xor(y[47], w187);
+    let w190 = c.and(w188, w189);
+    let w191 = c.xor(w190, w187);
+    let w192 = c.xor(x[48], w191);
+    let w193 = c.xor(y[48], w191);
+    let w194 = c.and(w192, w193);
+    let w195 = c.xor(w194, w191);
+    let w196 = c.xor(x[49], w195);
+    let w197 = c.xor(y[49], w195);
+    let w198 = c.and(w196, w197);
+    let w199 = c.xor(w198, w195);
+    let w200 = c.xor(x[50], w199);
+    let w201 = c.xor(y[50], w199);
+    let w202 = c.and(w200, w201);
+    let w203 = c.xor(w202, w199);
+    let w204 = c.xor(x[51], w203);
+    let w205 = c.xor(y[51], w203);
+    let w206 = c.and(w204, w205);
+    let w207 = c.xor(w206, w203);
+    let w208 = c.xor(x[52], w207);
+    let w209 = c.xor(y[52], w207);
+    let w210 = c.and(w208, w209);
+    let w211 = c.xor(w210, w207);
+    let w212 = c.xor(x[53], w211);
+    let w213 = c.xor(y[53], w211);
+    let w214 = c.and(w212, w213);
+    let w215 = c.xor(w214, w211);
+    let w216 = c.xor(x[54], w215);
+    let w217 = c.xor(y[54], w215);
+    let w218 = c.and(w216, w217);
+    let w219 = c.xor(w218, w215);
+    let w220 = c.xor(x[55], w219);
+    let w221 = c.xor(y[55], w219);
+    let w222 = c.and(w220, w221);
+    let w223 = c.xor(w222, w219);
+    let w224 = c.xor(x[56], w223);
+    let w225 = c.xor(y[56], w223);
+    let w226 = c.and(w224, w225);
+    let w227 = c.xor(w226, w223);
+    let w228 = c.xor(x[57], w227);
+    let w229 = c.xor(y[57], w227);
+    let w230 = c.and(w228, w229);
+    let w231 = c.xor(w230, w227);
+    let w232 = c.xor(x[58], w231);
+    let w233 = c.xor(y[58], w231);
+    let w234 = c.and(w232, w233);
+    let w235 = c.xor(w234, w231);
+    let w236 = c.xor(x[59], w235);
+    let w237 = c.xor(y[59], w235);
+    let w238 = c.and(w236, w237);
+    let w239 = c.xor(w238, w235);
+    let w240 = c.xor(x[60], w239);
+    let w241 = c.xor(y[60], w239);
+    let w242 = c.and(w240, w241);
+    let w243 = c.xor(w242, w239);
+    let w244 = c.xor(x[61], w243);
+    let w245 = c.xor(y[61], w243);
+    let w246 = c.and(w244, w245);
+    let w247 = c.xor(w246, w243);
+    let w248 = c.xor(x[62], w247);
+    let w249 = c.xor(y[62], w247);
+    let w250 = c.and(w248, w249);
+    let w251 = c.xor(w0, y[0]);
+    let w252 = c.xor(w4, y[1]);
+    let w253 = c.xor(w8, y[2]);
+    let w254 = c.xor(w12, y[3]);
+    let w255 = c.xor(w16, y[4]);
+    let w256 = c.xor(w20, y[5]);
+    let w257 = c.xor(w24, y[6]);
+    let w258 = c.xor(w28, y[7]);
+    let w259 = c.xor(w32, y[8]);
+    let w260 = c.xor(w36, y[9]);
+    let w261 = c.xor(w40, y[10]);
+    let w262 = c.xor(w44, y[11]);
+    let w263 = c.xor(w48, y[12]);
+    let w264 = c.xor(w52, y[13]);
+    let w265 = c.xor(w56, y[14]);
+    let w266 = c.xor(w60, y[15]);
+    let w267 = c.xor(w64, y[16]);
+    let w268 = c.xor(w68, y[17]);
+    let w269 = c.xor(w72, y[18]);
+    let w270 = c.xor(w76, y[19]);
+    let w271 = c.xor(w80, y[20]);
+    let w272 = c.xor(w84, y[21]);
+    let w273 = c.xor(w88, y[22]);
+    let w274 = c.xor(w92, y[23]);
+    let w275 = c.xor(w96, y[24]);
+    let w276 = c.xor(w100, y[25]);
+    let w277 = c.xor(w104, y[26]);
+    let w278 = c.xor(w108, y[27]);
+    let w279 = c.xor(w112, y[28]);
+    let w280 = c.xor(w116, y[29]);
+    let w281 = c.xor(w120, y[30]);
+    let w282 = c.xor(w124, y[31]);
+    let w283 = c.xor(w128, y[32]);
+    let w284 = c.xor(w132, y[33]);
+    let w285 = c.xor(w136, y[34]);
+    let w286 = c.xor(w140, y[35]);
+    let w287 = c.xor(w144, y[36]);
+    let w288 = c.xor(w148, y[37]);
+    let w289 = c.xor(w152, y[38]);
+    let w290 = c.xor(w156, y[39]);
+    let w291 = c.xor(w160, y[40]);
+    let w292 = c.xor(w164, y[41]);
+    let w293 = c.xor(w168, y[42]);
+    let w294 = c.xor(w172, y[43]);
+    let w295 = c.xor(w176, y[44]);
+    let w296 = c.xor(w180, y[45]);
+    let w297 = c.xor(w184, y[46]);
+    let w298 = c.xor(w188, y[47]);
+    let w299 = c.xor(w192, y[48]);
+    let w300 = c.xor(w196, y[49]);
+    let w301 = c.xor(w200, y[50]);
+    let w302 = c.xor(w204, y[51]);
+    let w303 = c.xor(w208, y[52]);
+    let w304 = c.xor(w212, y[53]);
+    let w305 = c.xor(w216, y[54]);
+    let w306 = c.xor(w220, y[55]);
+    let w307 = c.xor(w224, y[56]);
+    let w308 = c.xor(w228, y[57]);
+    let w309 = c.xor(w232, y[58]);
+    let w310 = c.xor(w236, y[59]);
+    let w311 = c.xor(w240, y[60]);
+    let w312 = c.xor(w244, y[61]);
+    let w313 = c.xor(w248, y[62]);
+    let w314 = c.xor(w250, w247);
+    let w315 = c.xor(x[63], w314);
+    let w316 = c.xor(w315, y[63]);
+    [
+        w251, w252, w253, w254, w255, w256, w257, w258, w259, w260, w261, w262, w263, w264, w265, w266, w267, w268,
+        w269, w270, w271, w272, w273, w274, w275, w276, w277, w278, w279, w280, w281, w282, w283, w284, w285, w286,
+        w287, w288, w289, w290, w291, w292, w293, w294, w295, w296, w297, w298, w299, w300, w301, w302, w303, w304,
+        w305, w306, w307, w308, w309, w310, w311, w312, w313, w316,
+    ]
+}
+
+/// The checked wrapping_add32 artifact, least-significant-bit products first.
+pub fn wrapping_add32(c: &mut Builder, x: &[Wire; 32], y: &[Wire; 32]) -> [Wire; 32] {
+    let w0 = c.xor(x[0], Wire::ZERO);
+    let w1 = c.xor(y[0], Wire::ZERO);
+    let w2 = c.and(w0, w1);
+    let w3 = c.xor(w2, Wire::ZERO);
+    let w4 = c.xor(x[1], w3);
+    let w5 = c.xor(y[1], w3);
+    let w6 = c.and(w4, w5);
+    let w7 = c.xor(w6, w3);
+    let w8 = c.xor(x[2], w7);
+    let w9 = c.xor(y[2], w7);
+    let w10 = c.and(w8, w9);
+    let w11 = c.xor(w10, w7);
+    let w12 = c.xor(x[3], w11);
+    let w13 = c.xor(y[3], w11);
+    let w14 = c.and(w12, w13);
+    let w15 = c.xor(w14, w11);
+    let w16 = c.xor(x[4], w15);
+    let w17 = c.xor(y[4], w15);
+    let w18 = c.and(w16, w17);
+    let w19 = c.xor(w18, w15);
+    let w20 = c.xor(x[5], w19);
+    let w21 = c.xor(y[5], w19);
+    let w22 = c.and(w20, w21);
+    let w23 = c.xor(w22, w19);
+    let w24 = c.xor(x[6], w23);
+    let w25 = c.xor(y[6], w23);
+    let w26 = c.and(w24, w25);
+    let w27 = c.xor(w26, w23);
+    let w28 = c.xor(x[7], w27);
+    let w29 = c.xor(y[7], w27);
+    let w30 = c.and(w28, w29);
+    let w31 = c.xor(w30, w27);
+    let w32 = c.xor(x[8], w31);
+    let w33 = c.xor(y[8], w31);
+    let w34 = c.and(w32, w33);
+    let w35 = c.xor(w34, w31);
+    let w36 = c.xor(x[9], w35);
+    let w37 = c.xor(y[9], w35);
+    let w38 = c.and(w36, w37);
+    let w39 = c.xor(w38, w35);
+    let w40 = c.xor(x[10], w39);
+    let w41 = c.xor(y[10], w39);
+    let w42 = c.and(w40, w41);
+    let w43 = c.xor(w42, w39);
+    let w44 = c.xor(x[11], w43);
+    let w45 = c.xor(y[11], w43);
+    let w46 = c.and(w44, w45);
+    let w47 = c.xor(w46, w43);
+    let w48 = c.xor(x[12], w47);
+    let w49 = c.xor(y[12], w47);
+    let w50 = c.and(w48, w49);
+    let w51 = c.xor(w50, w47);
+    let w52 = c.xor(x[13], w51);
+    let w53 = c.xor(y[13], w51);
+    let w54 = c.and(w52, w53);
+    let w55 = c.xor(w54, w51);
+    let w56 = c.xor(x[14], w55);
+    let w57 = c.xor(y[14], w55);
+    let w58 = c.and(w56, w57);
+    let w59 = c.xor(w58, w55);
+    let w60 = c.xor(x[15], w59);
+    let w61 = c.xor(y[15], w59);
+    let w62 = c.and(w60, w61);
+    let w63 = c.xor(w62, w59);
+    let w64 = c.xor(x[16], w63);
+    let w65 = c.xor(y[16], w63);
+    let w66 = c.and(w64, w65);
+    let w67 = c.xor(w66, w63);
+    let w68 = c.xor(x[17], w67);
+    let w69 = c.xor(y[17], w67);
+    let w70 = c.and(w68, w69);
+    let w71 = c.xor(w70, w67);
+    let w72 = c.xor(x[18], w71);
+    let w73 = c.xor(y[18], w71);
+    let w74 = c.and(w72, w73);
+    let w75 = c.xor(w74, w71);
+    let w76 = c.xor(x[19], w75);
+    let w77 = c.xor(y[19], w75);
+    let w78 = c.and(w76, w77);
+    let w79 = c.xor(w78, w75);
+    let w80 = c.xor(x[20], w79);
+    let w81 = c.xor(y[20], w79);
+    let w82 = c.and(w80, w81);
+    let w83 = c.xor(w82, w79);
+    let w84 = c.xor(x[21], w83);
+    let w85 = c.xor(y[21], w83);
+    let w86 = c.and(w84, w85);
+    let w87 = c.xor(w86, w83);
+    let w88 = c.xor(x[22], w87);
+    let w89 = c.xor(y[22], w87);
+    let w90 = c.and(w88, w89);
+    let w91 = c.xor(w90, w87);
+    let w92 = c.xor(x[23], w91);
+    let w93 = c.xor(y[23], w91);
+    let w94 = c.and(w92, w93);
+    let w95 = c.xor(w94, w91);
+    let w96 = c.xor(x[24], w95);
+    let w97 = c.xor(y[24], w95);
+    let w98 = c.and(w96, w97);
+    let w99 = c.xor(w98, w95);
+    let w100 = c.xor(x[25], w99);
+    let w101 = c.xor(y[25], w99);
+    let w102 = c.and(w100, w101);
+    let w103 = c.xor(w102, w99);
+    let w104 = c.xor(x[26], w103);
+    let w105 = c.xor(y[26], w103);
+    let w106 = c.and(w104, w105);
+    let w107 = c.xor(w106, w103);
+    let w108 = c.xor(x[27], w107);
+    let w109 = c.xor(y[27], w107);
+    let w110 = c.and(w108, w109);
+    let w111 = c.xor(w110, w107);
+    let w112 = c.xor(x[28], w111);
+    let w113 = c.xor(y[28], w111);
+    let w114 = c.and(w112, w113);
+    let w115 = c.xor(w114, w111);
+    let w116 = c.xor(x[29], w115);
+    let w117 = c.xor(y[29], w115);
+    let w118 = c.and(w116, w117);
+    let w119 = c.xor(w118, w115);
+    let w120 = c.xor(x[30], w119);
+    let w121 = c.xor(y[30], w119);
+    let w122 = c.and(w120, w121);
+    let w123 = c.xor(w0, y[0]);
+    let w124 = c.xor(w4, y[1]);
+    let w125 = c.xor(w8, y[2]);
+    let w126 = c.xor(w12, y[3]);
+    let w127 = c.xor(w16, y[4]);
+    let w128 = c.xor(w20, y[5]);
+    let w129 = c.xor(w24, y[6]);
+    let w130 = c.xor(w28, y[7]);
+    let w131 = c.xor(w32, y[8]);
+    let w132 = c.xor(w36, y[9]);
+    let w133 = c.xor(w40, y[10]);
+    let w134 = c.xor(w44, y[11]);
+    let w135 = c.xor(w48, y[12]);
+    let w136 = c.xor(w52, y[13]);
+    let w137 = c.xor(w56, y[14]);
+    let w138 = c.xor(w60, y[15]);
+    let w139 = c.xor(w64, y[16]);
+    let w140 = c.xor(w68, y[17]);
+    let w141 = c.xor(w72, y[18]);
+    let w142 = c.xor(w76, y[19]);
+    let w143 = c.xor(w80, y[20]);
+    let w144 = c.xor(w84, y[21]);
+    let w145 = c.xor(w88, y[22]);
+    let w146 = c.xor(w92, y[23]);
+    let w147 = c.xor(w96, y[24]);
+    let w148 = c.xor(w100, y[25]);
+    let w149 = c.xor(w104, y[26]);
+    let w150 = c.xor(w108, y[27]);
+    let w151 = c.xor(w112, y[28]);
+    let w152 = c.xor(w116, y[29]);
+    let w153 = c.xor(w120, y[30]);
+    let w154 = c.xor(w122, w119);
+    let w155 = c.xor(x[31], w154);
+    let w156 = c.xor(w155, y[31]);
+    [
+        w123, w124, w125, w126, w127, w128, w129, w130, w131, w132, w133, w134, w135, w136, w137, w138, w139, w140,
+        w141, w142, w143, w144, w145, w146, w147, w148, w149, w150, w151, w152, w153, w156,
+    ]
+}
+
+/// The checked add_with_carry64 artifact, least-significant-bit products first.
+pub fn add_with_carry64(c: &mut Builder, x: &[Wire; 64], y: &[Wire; 64], carry_in: Wire) -> ([Wire; 64], Wire) {
+    let w0 = c.xor(x[0], carry_in);
+    let w1 = c.xor(y[0], carry_in);
+    let w2 = c.and(w0, w1);
+    let w3 = c.xor(w2, carry_in);
+    let w4 = c.xor(x[1], w3);
+    let w5 = c.xor(y[1], w3);
+    let w6 = c.and(w4, w5);
+    let w7 = c.xor(w6, w3);
+    let w8 = c.xor(x[2], w7);
+    let w9 = c.xor(y[2], w7);
+    let w10 = c.and(w8, w9);
+    let w11 = c.xor(w10, w7);
+    let w12 = c.xor(x[3], w11);
+    let w13 = c.xor(y[3], w11);
+    let w14 = c.and(w12, w13);
+    let w15 = c.xor(w14, w11);
+    let w16 = c.xor(x[4], w15);
+    let w17 = c.xor(y[4], w15);
+    let w18 = c.and(w16, w17);
+    let w19 = c.xor(w18, w15);
+    let w20 = c.xor(x[5], w19);
+    let w21 = c.xor(y[5], w19);
+    let w22 = c.and(w20, w21);
+    let w23 = c.xor(w22, w19);
+    let w24 = c.xor(x[6], w23);
+    let w25 = c.xor(y[6], w23);
+    let w26 = c.and(w24, w25);
+    let w27 = c.xor(w26, w23);
+    let w28 = c.xor(x[7], w27);
+    let w29 = c.xor(y[7], w27);
+    let w30 = c.and(w28, w29);
+    let w31 = c.xor(w30, w27);
+    let w32 = c.xor(x[8], w31);
+    let w33 = c.xor(y[8], w31);
+    let w34 = c.and(w32, w33);
+    let w35 = c.xor(w34, w31);
+    let w36 = c.xor(x[9], w35);
+    let w37 = c.xor(y[9], w35);
+    let w38 = c.and(w36, w37);
+    let w39 = c.xor(w38, w35);
+    let w40 = c.xor(x[10], w39);
+    let w41 = c.xor(y[10], w39);
+    let w42 = c.and(w40, w41);
+    let w43 = c.xor(w42, w39);
+    let w44 = c.xor(x[11], w43);
+    let w45 = c.xor(y[11], w43);
+    let w46 = c.and(w44, w45);
+    let w47 = c.xor(w46, w43);
+    let w48 = c.xor(x[12], w47);
+    let w49 = c.xor(y[12], w47);
+    let w50 = c.and(w48, w49);
+    let w51 = c.xor(w50, w47);
+    let w52 = c.xor(x[13], w51);
+    let w53 = c.xor(y[13], w51);
+    let w54 = c.and(w52, w53);
+    let w55 = c.xor(w54, w51);
+    let w56 = c.xor(x[14], w55);
+    let w57 = c.xor(y[14], w55);
+    let w58 = c.and(w56, w57);
+    let w59 = c.xor(w58, w55);
+    let w60 = c.xor(x[15], w59);
+    let w61 = c.xor(y[15], w59);
+    let w62 = c.and(w60, w61);
+    let w63 = c.xor(w62, w59);
+    let w64 = c.xor(x[16], w63);
+    let w65 = c.xor(y[16], w63);
+    let w66 = c.and(w64, w65);
+    let w67 = c.xor(w66, w63);
+    let w68 = c.xor(x[17], w67);
+    let w69 = c.xor(y[17], w67);
+    let w70 = c.and(w68, w69);
+    let w71 = c.xor(w70, w67);
+    let w72 = c.xor(x[18], w71);
+    let w73 = c.xor(y[18], w71);
+    let w74 = c.and(w72, w73);
+    let w75 = c.xor(w74, w71);
+    let w76 = c.xor(x[19], w75);
+    let w77 = c.xor(y[19], w75);
+    let w78 = c.and(w76, w77);
+    let w79 = c.xor(w78, w75);
+    let w80 = c.xor(x[20], w79);
+    let w81 = c.xor(y[20], w79);
+    let w82 = c.and(w80, w81);
+    let w83 = c.xor(w82, w79);
+    let w84 = c.xor(x[21], w83);
+    let w85 = c.xor(y[21], w83);
+    let w86 = c.and(w84, w85);
+    let w87 = c.xor(w86, w83);
+    let w88 = c.xor(x[22], w87);
+    let w89 = c.xor(y[22], w87);
+    let w90 = c.and(w88, w89);
+    let w91 = c.xor(w90, w87);
+    let w92 = c.xor(x[23], w91);
+    let w93 = c.xor(y[23], w91);
+    let w94 = c.and(w92, w93);
+    let w95 = c.xor(w94, w91);
+    let w96 = c.xor(x[24], w95);
+    let w97 = c.xor(y[24], w95);
+    let w98 = c.and(w96, w97);
+    let w99 = c.xor(w98, w95);
+    let w100 = c.xor(x[25], w99);
+    let w101 = c.xor(y[25], w99);
+    let w102 = c.and(w100, w101);
+    let w103 = c.xor(w102, w99);
+    let w104 = c.xor(x[26], w103);
+    let w105 = c.xor(y[26], w103);
+    let w106 = c.and(w104, w105);
+    let w107 = c.xor(w106, w103);
+    let w108 = c.xor(x[27], w107);
+    let w109 = c.xor(y[27], w107);
+    let w110 = c.and(w108, w109);
+    let w111 = c.xor(w110, w107);
+    let w112 = c.xor(x[28], w111);
+    let w113 = c.xor(y[28], w111);
+    let w114 = c.and(w112, w113);
+    let w115 = c.xor(w114, w111);
+    let w116 = c.xor(x[29], w115);
+    let w117 = c.xor(y[29], w115);
+    let w118 = c.and(w116, w117);
+    let w119 = c.xor(w118, w115);
+    let w120 = c.xor(x[30], w119);
+    let w121 = c.xor(y[30], w119);
+    let w122 = c.and(w120, w121);
+    let w123 = c.xor(w122, w119);
+    let w124 = c.xor(x[31], w123);
+    let w125 = c.xor(y[31], w123);
+    let w126 = c.and(w124, w125);
+    let w127 = c.xor(w126, w123);
+    let w128 = c.xor(x[32], w127);
+    let w129 = c.xor(y[32], w127);
+    let w130 = c.and(w128, w129);
+    let w131 = c.xor(w130, w127);
+    let w132 = c.xor(x[33], w131);
+    let w133 = c.xor(y[33], w131);
+    let w134 = c.and(w132, w133);
+    let w135 = c.xor(w134, w131);
+    let w136 = c.xor(x[34], w135);
+    let w137 = c.xor(y[34], w135);
+    let w138 = c.and(w136, w137);
+    let w139 = c.xor(w138, w135);
+    let w140 = c.xor(x[35], w139);
+    let w141 = c.xor(y[35], w139);
+    let w142 = c.and(w140, w141);
+    let w143 = c.xor(w142, w139);
+    let w144 = c.xor(x[36], w143);
+    let w145 = c.xor(y[36], w143);
+    let w146 = c.and(w144, w145);
+    let w147 = c.xor(w146, w143);
+    let w148 = c.xor(x[37], w147);
+    let w149 = c.xor(y[37], w147);
+    let w150 = c.and(w148, w149);
+    let w151 = c.xor(w150, w147);
+    let w152 = c.xor(x[38], w151);
+    let w153 = c.xor(y[38], w151);
+    let w154 = c.and(w152, w153);
+    let w155 = c.xor(w154, w151);
+    let w156 = c.xor(x[39], w155);
+    let w157 = c.xor(y[39], w155);
+    let w158 = c.and(w156, w157);
+    let w159 = c.xor(w158, w155);
+    let w160 = c.xor(x[40], w159);
+    let w161 = c.xor(y[40], w159);
+    let w162 = c.and(w160, w161);
+    let w163 = c.xor(w162, w159);
+    let w164 = c.xor(x[41], w163);
+    let w165 = c.xor(y[41], w163);
+    let w166 = c.and(w164, w165);
+    let w167 = c.xor(w166, w163);
+    let w168 = c.xor(x[42], w167);
+    let w169 = c.xor(y[42], w167);
+    let w170 = c.and(w168, w169);
+    let w171 = c.xor(w170, w167);
+    let w172 = c.xor(x[43], w171);
+    let w173 = c.xor(y[43], w171);
+    let w174 = c.and(w172, w173);
+    let w175 = c.xor(w174, w171);
+    let w176 = c.xor(x[44], w175);
+    let w177 = c.xor(y[44], w175);
+    let w178 = c.and(w176, w177);
+    let w179 = c.xor(w178, w175);
+    let w180 = c.xor(x[45], w179);
+    let w181 = c.xor(y[45], w179);
+    let w182 = c.and(w180, w181);
+    let w183 = c.xor(w182, w179);
+    let w184 = c.xor(x[46], w183);
+    let w185 = c.xor(y[46], w183);
+    let w186 = c.and(w184, w185);
+    let w187 = c.xor(w186, w183);
+    let w188 = c.xor(x[47], w187);
+    let w189 = c.xor(y[47], w187);
+    let w190 = c.and(w188, w189);
+    let w191 = c.xor(w190, w187);
+    let w192 = c.xor(x[48], w191);
+    let w193 = c.xor(y[48], w191);
+    let w194 = c.and(w192, w193);
+    let w195 = c.xor(w194, w191);
+    let w196 = c.xor(x[49], w195);
+    let w197 = c.xor(y[49], w195);
+    let w198 = c.and(w196, w197);
+    let w199 = c.xor(w198, w195);
+    let w200 = c.xor(x[50], w199);
+    let w201 = c.xor(y[50], w199);
+    let w202 = c.and(w200, w201);
+    let w203 = c.xor(w202, w199);
+    let w204 = c.xor(x[51], w203);
+    let w205 = c.xor(y[51], w203);
+    let w206 = c.and(w204, w205);
+    let w207 = c.xor(w206, w203);
+    let w208 = c.xor(x[52], w207);
+    let w209 = c.xor(y[52], w207);
+    let w210 = c.and(w208, w209);
+    let w211 = c.xor(w210, w207);
+    let w212 = c.xor(x[53], w211);
+    let w213 = c.xor(y[53], w211);
+    let w214 = c.and(w212, w213);
+    let w215 = c.xor(w214, w211);
+    let w216 = c.xor(x[54], w215);
+    let w217 = c.xor(y[54], w215);
+    let w218 = c.and(w216, w217);
+    let w219 = c.xor(w218, w215);
+    let w220 = c.xor(x[55], w219);
+    let w221 = c.xor(y[55], w219);
+    let w222 = c.and(w220, w221);
+    let w223 = c.xor(w222, w219);
+    let w224 = c.xor(x[56], w223);
+    let w225 = c.xor(y[56], w223);
+    let w226 = c.and(w224, w225);
+    let w227 = c.xor(w226, w223);
+    let w228 = c.xor(x[57], w227);
+    let w229 = c.xor(y[57], w227);
+    let w230 = c.and(w228, w229);
+    let w231 = c.xor(w230, w227);
+    let w232 = c.xor(x[58], w231);
+    let w233 = c.xor(y[58], w231);
+    let w234 = c.and(w232, w233);
+    let w235 = c.xor(w234, w231);
+    let w236 = c.xor(x[59], w235);
+    let w237 = c.xor(y[59], w235);
+    let w238 = c.and(w236, w237);
+    let w239 = c.xor(w238, w235);
+    let w240 = c.xor(x[60], w239);
+    let w241 = c.xor(y[60], w239);
+    let w242 = c.and(w240, w241);
+    let w243 = c.xor(w242, w239);
+    let w244 = c.xor(x[61], w243);
+    let w245 = c.xor(y[61], w243);
+    let w246 = c.and(w244, w245);
+    let w247 = c.xor(w246, w243);
+    let w248 = c.xor(x[62], w247);
+    let w249 = c.xor(y[62], w247);
+    let w250 = c.and(w248, w249);
+    let w251 = c.xor(w250, w247);
+    let w252 = c.xor(x[63], w251);
+    let w253 = c.xor(y[63], w251);
+    let w254 = c.and(w252, w253);
+    let w255 = c.xor(w0, y[0]);
+    let w256 = c.xor(w4, y[1]);
+    let w257 = c.xor(w8, y[2]);
+    let w258 = c.xor(w12, y[3]);
+    let w259 = c.xor(w16, y[4]);
+    let w260 = c.xor(w20, y[5]);
+    let w261 = c.xor(w24, y[6]);
+    let w262 = c.xor(w28, y[7]);
+    let w263 = c.xor(w32, y[8]);
+    let w264 = c.xor(w36, y[9]);
+    let w265 = c.xor(w40, y[10]);
+    let w266 = c.xor(w44, y[11]);
+    let w267 = c.xor(w48, y[12]);
+    let w268 = c.xor(w52, y[13]);
+    let w269 = c.xor(w56, y[14]);
+    let w270 = c.xor(w60, y[15]);
+    let w271 = c.xor(w64, y[16]);
+    let w272 = c.xor(w68, y[17]);
+    let w273 = c.xor(w72, y[18]);
+    let w274 = c.xor(w76, y[19]);
+    let w275 = c.xor(w80, y[20]);
+    let w276 = c.xor(w84, y[21]);
+    let w277 = c.xor(w88, y[22]);
+    let w278 = c.xor(w92, y[23]);
+    let w279 = c.xor(w96, y[24]);
+    let w280 = c.xor(w100, y[25]);
+    let w281 = c.xor(w104, y[26]);
+    let w282 = c.xor(w108, y[27]);
+    let w283 = c.xor(w112, y[28]);
+    let w284 = c.xor(w116, y[29]);
+    let w285 = c.xor(w120, y[30]);
+    let w286 = c.xor(w124, y[31]);
+    let w287 = c.xor(w128, y[32]);
+    let w288 = c.xor(w132, y[33]);
+    let w289 = c.xor(w136, y[34]);
+    let w290 = c.xor(w140, y[35]);
+    let w291 = c.xor(w144, y[36]);
+    let w292 = c.xor(w148, y[37]);
+    let w293 = c.xor(w152, y[38]);
+    let w294 = c.xor(w156, y[39]);
+    let w295 = c.xor(w160, y[40]);
+    let w296 = c.xor(w164, y[41]);
+    let w297 = c.xor(w168, y[42]);
+    let w298 = c.xor(w172, y[43]);
+    let w299 = c.xor(w176, y[44]);
+    let w300 = c.xor(w180, y[45]);
+    let w301 = c.xor(w184, y[46]);
+    let w302 = c.xor(w188, y[47]);
+    let w303 = c.xor(w192, y[48]);
+    let w304 = c.xor(w196, y[49]);
+    let w305 = c.xor(w200, y[50]);
+    let w306 = c.xor(w204, y[51]);
+    let w307 = c.xor(w208, y[52]);
+    let w308 = c.xor(w212, y[53]);
+    let w309 = c.xor(w216, y[54]);
+    let w310 = c.xor(w220, y[55]);
+    let w311 = c.xor(w224, y[56]);
+    let w312 = c.xor(w228, y[57]);
+    let w313 = c.xor(w232, y[58]);
+    let w314 = c.xor(w236, y[59]);
+    let w315 = c.xor(w240, y[60]);
+    let w316 = c.xor(w244, y[61]);
+    let w317 = c.xor(w248, y[62]);
+    let w318 = c.xor(w252, y[63]);
+    let w319 = c.xor(w254, w251);
+    (
+        [
+            w255, w256, w257, w258, w259, w260, w261, w262, w263, w264, w265, w266, w267, w268, w269, w270, w271, w272,
+            w273, w274, w275, w276, w277, w278, w279, w280, w281, w282, w283, w284, w285, w286, w287, w288, w289, w290,
+            w291, w292, w293, w294, w295, w296, w297, w298, w299, w300, w301, w302, w303, w304, w305, w306, w307, w308,
+            w309, w310, w311, w312, w313, w314, w315, w316, w317, w318,
+        ],
+        w319,
+    )
+}
diff --git a/crates/flock/src/lib.rs b/crates/flock/src/lib.rs
index cba158eff..4e3ad0ec3 100644
--- a/crates/flock/src/lib.rs
+++ b/crates/flock/src/lib.rs
@@ -20,6 +20,7 @@
 #![warn(unreachable_pub)]
 
 pub mod circuit;
+pub mod clean;
 mod error;
 pub mod gadgets;
 pub mod lincheck;
diff --git a/crates/flock/src/reduction.rs b/crates/flock/src/reduction.rs
index c24ffc72f..d441157eb 100644
--- a/crates/flock/src/reduction.rs
+++ b/crates/flock/src/reduction.rs
@@ -293,7 +293,7 @@ mod tests {
     use primitives::test_util::Rng;
 
     use crate::Witness;
-    use crate::circuit::{Builder, Circuit, Wire};
+    use crate::circuit::{Builder, Circuit};
     use crate::gadgets::Multiplier;
     use crate::reduction::{self, Block, Instance};
     use crate::zerocheck::K_SKIP;
@@ -327,7 +327,7 @@ mod tests {
             let mut c = Builder::new(&[64, 64], &[n]);
             let (a, b) = (c.input(0), c.input(1));
             let out = match self {
-                Self::WrappingAdd => ripple_carry(&mut c, &a, &b).to_vec(),
+                Self::WrappingAdd => crate::clean::wrapping_add64(&mut c, &a, &b).to_vec(),
                 Self::WrappingMul => Multiplier::build::<64>(&mut c, &a, &b).0.to_vec(),
                 Self::WideningMul => Multiplier::build::<128>(&mut c, &a, &b).0.to_vec(),
             };
@@ -338,23 +338,6 @@ mod tests {
         }
     }
 
-    /// `a + b mod 2^64`: the carry into bit `i + 1` is `maj(a_i, b_i, c_i) = (a_i + c_i)(b_i + c_i) + c_i`.
-    fn ripple_carry(c: &mut Builder, a: &[Wire; 64], b: &[Wire; 64]) -> [Wire; 64] {
-        let mut carry = Wire::ZERO;
-        let mut sum = [Wire::ZERO; 64];
-        for i in 0..64 {
-            let ac = c.xor(a[i], carry);
-            let bc = c.xor(b[i], carry);
-            sum[i] = c.xor(ac, b[i]);
-            // The carry out of bit 63 falls off the modulus.
-            if i < 63 {
-                let maj = c.and(ac, bc);
-                carry = c.xor(maj, carry);
-            }
-        }
-        sum
-    }
-
     /// Every pairing of the carry-heavy edge values, then random pairs.
     fn pairs(n: usize, seed: u64) -> Vec<[u64; 2]> {
         const EDGES: [u64; 6] = [0, 1, 2, 1 << 63, u64::MAX - 1, u64::MAX];
diff --git a/crates/leanvm_core/src/rv/circuits.rs b/crates/leanvm_core/src/rv/circuits.rs
index a530a732e..25aac4160 100644
--- a/crates/leanvm_core/src/rv/circuits.rs
+++ b/crates/leanvm_core/src/rv/circuits.rs
@@ -34,14 +34,8 @@ pub(super) trait WordGadgets {
     /// Whether any bit of `x` is set; one product per OR.
     fn any(&mut self, x: &[Wire]) -> Wire;
 
-    /// `x + y + carry_in`, and the carry out of the top bit; one product per bit.
-    fn add_with_carry<const N: usize>(&mut self, x: &[Wire; N], y: &[Wire; N], carry_in: Wire) -> ([Wire; N], Wire);
-
-    /// `x + y` modulo `2^N`; one product per bit but the top.
-    fn add_wrapping<const N: usize>(&mut self, x: &[Wire; N], y: &[Wire; N]) -> [Wire; N];
-
     /// `-x` if `negative`, else `x`; one product per bit.
-    fn negate_if<const N: usize>(&mut self, negative: Wire, x: &[Wire; N]) -> [Wire; N];
+    fn negate_if(&mut self, negative: Wire, x: &[Wire; 64]) -> [Wire; 64];
 
     /// `x`, bits 32 to 63 replaced by bit 31 when `word` is set; one product per high bit.
     fn sext32_if(&mut self, word: Wire, x: &[Wire; 64]) -> [Wire; 64];
@@ -81,43 +75,10 @@ impl WordGadgets for Builder {
         x.iter().fold(Wire::ZERO, |acc, &bit| self.or(acc, bit))
     }
 
-    fn add_with_carry<const N: usize>(&mut self, x: &[Wire; N], y: &[Wire; N], carry_in: Wire) -> ([Wire; N], Wire) {
-        let mut carry = carry_in;
-        let sum = std::array::from_fn(|i| {
-            // The sum bit is x ^ y ^ c.
-            let xc = self.xor(x[i], carry);
-            let yc = self.xor(y[i], carry);
-            let sum = self.xor(xc, y[i]);
-
-            // The carry out is maj(x, y, c) = ((x ^ c)(y ^ c)) ^ c.
-            let maj = self.and(xc, yc);
-            carry = self.xor(maj, carry);
-            sum
-        });
-        (sum, carry)
-    }
-
-    fn add_wrapping<const N: usize>(&mut self, x: &[Wire; N], y: &[Wire; N]) -> [Wire; N] {
-        let mut carry = Wire::ZERO;
-        std::array::from_fn(|i| {
-            // The sum bit is x ^ y ^ c.
-            let xc = self.xor(x[i], carry);
-            let yc = self.xor(y[i], carry);
-            let sum = self.xor(xc, y[i]);
-
-            // The carry out of the top bit falls off the modulus, so it is never made.
-            if i + 1 < N {
-                let maj = self.and(xc, yc);
-                carry = self.xor(maj, carry);
-            }
-            sum
-        })
-    }
-
-    fn negate_if<const N: usize>(&mut self, negative: Wire, x: &[Wire; N]) -> [Wire; N] {
+    fn negate_if(&mut self, negative: Wire, x: &[Wire; 64]) -> [Wire; 64] {
         // Two's complement: (x ^ negative) + negative.
         let flipped = x.map(|bit| self.xor(bit, negative));
-        self.add_with_carry(&flipped, &[Wire::ZERO; N], negative).0
+        flock::clean::add_with_carry64(self, &flipped, &[Wire::ZERO; 64], negative).0
     }
 
     fn sext32_if(&mut self, word: Wire, x: &[Wire; 64]) -> [Wire; 64] {
diff --git a/crates/leanvm_core/src/rv/semantics/alu.rs b/crates/leanvm_core/src/rv/semantics/alu.rs
index 73fe3daf6..99128dc1c 100644
--- a/crates/leanvm_core/src/rv/semantics/alu.rs
+++ b/crates/leanvm_core/src/rv/semantics/alu.rs
@@ -178,7 +178,7 @@ impl ClassCircuit for Alu {
         // It borrows exactly when that sum does not carry out.
         let sub = flag(Self::SUB);
         let b_or_not = b.map(|bit| c.xor(bit, sub));
-        let (sum, carry_out) = c.add_with_carry(&v1, &b_or_not, sub);
+        let (sum, carry_out) = flock::clean::add_with_carry64(&mut c, &v1, &b_or_not, sub);
 
         // The comparisons, from the borrow and the signs.
         //
diff --git a/crates/leanvm_core/src/rv/semantics/divide.rs b/crates/leanvm_core/src/rv/semantics/divide.rs
index 633047e5f..321c2101a 100644
--- a/crates/leanvm_core/src/rv/semantics/divide.rs
+++ b/crates/leanvm_core/src/rv/semantics/divide.rs
@@ -124,13 +124,13 @@ impl ClassCircuit for Div {
         let low: [Wire; 64] = std::array::from_fn(|i| product[i]);
         let high: [Wire; 64] = std::array::from_fn(|i| product[64 + i]);
         let overflows = c.any(&high);
-        let (sum, carries) = c.add_with_carry(&low, &r, Wire::ZERO);
+        let (sum, carries) = flock::clean::add_with_carry64(&mut c, &low, &r, Wire::ZERO);
         let difference = c.xor_word(&sum, &n_abs);
         let differs = c.any(&difference);
 
         // Check r < |d|: r - |d| = r + !|d| + 1 carries out exactly when r >= |d|.
         let d_inverted = d_abs.map(|bit| c.not(bit));
-        let (_, too_large) = c.add_with_carry(&r, &d_inverted, Wire::ONE);
+        let (_, too_large) = flock::clean::add_with_carry64(&mut c, &r, &d_inverted, Wire::ONE);
 
         // Any failed check is bad, unless the divisor is zero.
         let d_nonzero = c.any(&d);
diff --git a/crates/leanvm_core/src/rv/semantics/hash.rs b/crates/leanvm_core/src/rv/semantics/hash.rs
index 74f4b96ca..ef3497897 100644
--- a/crates/leanvm_core/src/rv/semantics/hash.rs
+++ b/crates/leanvm_core/src/rv/semantics/hash.rs
@@ -119,11 +119,11 @@ impl ClassCircuit for Hash {
         for round in &SIGMA {
             for (g, &[a, b, cc, d]) in G_LANES.iter().enumerate() {
                 for (x, r1, r2) in [(&m[round[2 * g]], 16, 12), (&m[round[2 * g + 1]], 8, 7)] {
-                    let ab = c.add_wrapping(&v[a], &v[b]);
-                    v[a] = c.add_wrapping(&ab, x);
+                    let ab = flock::clean::wrapping_add32(&mut c, &v[a], &v[b]);
+                    v[a] = flock::clean::wrapping_add32(&mut c, &ab, x);
                     let da = c.xor_word(&v[d], &v[a]);
                     v[d] = rotr(&da, r1);
-                    v[cc] = c.add_wrapping(&v[cc], &v[d]);
+                    v[cc] = flock::clean::wrapping_add32(&mut c, &v[cc], &v[d]);
                     let bc = c.xor_word(&v[b], &v[cc]);
                     v[b] = rotr(&bc, r2);
                 }
diff --git a/crates/leanvm_core/src/rv/semantics/memory.rs b/crates/leanvm_core/src/rv/semantics/memory.rs
index 3d3841c94..b8b7efaa0 100644
--- a/crates/leanvm_core/src/rv/semantics/memory.rs
+++ b/crates/leanvm_core/src/rv/semantics/memory.rs
@@ -195,7 +195,7 @@ impl ClassCircuit for Load {
         let [v1, imm] = [0, 1].map(|port| c.input::<64>(port));
         let flags = c.input::<3>(2);
         let cell = c.input::<64>(3);
-        let address = c.add_wrapping(&v1, &imm);
+        let address = flock::clean::wrapping_add64(&mut c, &v1, &imm);
         let [ge2, ge4] = c.width_thresholds([flags[0], flags[1]]);
         let bus = c.bus_address(&address, [ge2, ge4]);
 
@@ -246,7 +246,7 @@ impl ClassCircuit for Store {
         let [v1, v2, imm] = [0, 1, 2].map(|port| c.input::<64>(port));
         let flags = c.input::<2>(3);
         let cell = c.input::<64>(4);
-        let address = c.add_wrapping(&v1, &imm);
+        let address = flock::clean::wrapping_add64(&mut c, &v1, &imm);
         let [ge2, ge4] = c.width_thresholds(flags);
         let bus = c.bus_address(&address, [ge2, ge4]);
 
@@ -290,7 +290,7 @@ impl ClassCircuit for Ld {
     fn circuit() -> Circuit {
         let mut c = Builder::new(&[64, 64], &[64]);
         let [v1, imm] = [0, 1].map(|port| c.input::<64>(port));
-        let address = c.add_wrapping(&v1, &imm);
+        let address = flock::clean::wrapping_add64(&mut c, &v1, &imm);
         c.output_word(0, &address);
         c.finish()
     }
diff --git a/crates/leanvm_core/src/rv/semantics/multiply.rs b/crates/leanvm_core/src/rv/semantics/multiply.rs
index 4e28d3cf0..0079f6745 100644
--- a/crates/leanvm_core/src/rv/semantics/multiply.rs
+++ b/crates/leanvm_core/src/rv/semantics/multiply.rs
@@ -116,7 +116,7 @@ impl ClassCircuit for Mulh {
                 let inverted = c.not(bit);
                 c.and(negative, inverted)
             });
-            (high, _) = c.add_with_carry(&high, &subtrahend, negative);
+            (high, _) = flock::clean::add_with_carry64(&mut c, &high, &subtrahend, negative);
         }
 
         c.output_word(0, &high);
diff --git a/crates/leanvm_core/tests/verifiers/programs.rs b/crates/leanvm_core/tests/verifiers/programs.rs
index 77f043651..118653ec8 100644
--- a/crates/leanvm_core/tests/verifiers/programs.rs
+++ b/crates/leanvm_core/tests/verifiers/programs.rs
@@ -169,6 +169,45 @@ fn loads_and_stores_prove_and_verify() {
     proves_and_verifies("memory", &program, expected);
 }
 
+#[test]
+fn clean_adder_memory_addresses_wrap_and_carry() {
+    // The negative immediate overflows u64 addition; the positive one crosses a long carry chain.
+    // Both address the same RAM cell through the actual Ld/Sd production circuit and word witness.
+    let base = Region::RAM.base();
+    let text = Asm::new()
+        .li(Reg::T0, base + 8)
+        .li(Reg::T1, base - 8)
+        .load(Ld, Reg::A0, -8, Reg::T0)
+        .load(Ld, Reg::A1, 8, Reg::T1)
+        .store(Sd, Reg::A1, -8, Reg::T0)
+        .load(Ld, Reg::A2, 8, Reg::T1)
+        .li(Reg::A3, 0)
+        .exit()
+        .finish();
+    let program = Program::new(&text, Region::TEXT.base(), vec![9], 3, 0).expect("valid memory program");
+    proves_and_verifies("clean wrapping adder", &program, [9, 9, 9, 0]);
+}
+
+#[test]
+fn clean_carry_adder_arithmetic_boundaries() {
+    // Carry-in and final carry feed comparison, signed division, and signed high multiplication.
+    let text = Asm::new()
+        .li(Reg::T0, u64::MAX)
+        .li(Reg::T1, 1)
+        .r(Add, Reg::A0, Reg::T0, Reg::T1)
+        .r(Sltu, Reg::A1, Reg::T0, Reg::T1)
+        .li(Reg::T2, 1 << 63)
+        .li(Reg::T3, u64::MAX)
+        .r(Div, Reg::A2, Reg::T2, Reg::T3)
+        .li(Reg::T0, u64::MAX - 1)
+        .li(Reg::T1, 3)
+        .r(Mulh, Reg::A3, Reg::T0, Reg::T1)
+        .exit()
+        .finish();
+    let program = Program::new(&text, Region::TEXT.base(), vec![], 3, 0).expect("valid arithmetic program");
+    proves_and_verifies("clean carry adder", &program, [0, 0, 1 << 63, u64::MAX]);
+}
+
 /// Every shift and every multiplication, registers and immediates, 64-bit and 32-bit
 /// forms, folded into the output.
 #[test]
diff --git a/verification/circuits/Audit.lean b/verification/circuits/Audit.lean
new file mode 100644
index 000000000..3a96a28b9
--- /dev/null
+++ b/verification/circuits/Audit.lean
@@ -0,0 +1,44 @@
+import LeanVMCircuits
+
+#print axioms LeanVMCircuits.FullAdder.soundness
+#print axioms LeanVMCircuits.FullAdder.completeness
+#print axioms LeanVMCircuits.Flock.lowerAffine_correct
+#print axioms LeanVMCircuits.Flock.lower_correct
+#print axioms LeanVMCircuits.Flock.flatten_correct
+#print axioms LeanVMCircuits.Flock.adder64_source
+#print axioms LeanVMCircuits.Flock.adder64_layout
+#print axioms LeanVMCircuits.Flock.adder64_soundness
+#print axioms LeanVMCircuits.Flock.adder64_wellFormed
+#print axioms LeanVMCircuits.Flock.adder64_complete
+#print axioms LeanVMCircuits.Flock.lookup_rejected
+#print axioms LeanVMCircuits.Flock.interaction_rejected
+
+#print axioms LeanVMCircuits.Flock.adder32_source
+#print axioms LeanVMCircuits.Flock.adder32_soundness
+#print axioms LeanVMCircuits.Flock.adder32_layout
+#print axioms LeanVMCircuits.Flock.adder32_wellFormed
+#print axioms LeanVMCircuits.Flock.adder32_complete
+#print axioms LeanVMCircuits.Flock.carryAdder64_source
+#print axioms LeanVMCircuits.Flock.carryAdder64_soundness
+#print axioms LeanVMCircuits.Flock.carryAdder64_layout
+#print axioms LeanVMCircuits.Flock.carryAdder64_wellFormed
+#print axioms LeanVMCircuits.Flock.carryAdder64_complete
+
+open Lean Elab Command in
+run_cmd do
+  for theoremName in #[
+    ``LeanVMCircuits.FullAdder.soundness, ``LeanVMCircuits.FullAdder.completeness,
+    ``LeanVMCircuits.Flock.lowerAffine_correct, ``LeanVMCircuits.Flock.lower_correct,
+    ``LeanVMCircuits.Flock.flatten_correct, ``LeanVMCircuits.Flock.adder64_source,
+    ``LeanVMCircuits.Flock.adder64_layout, ``LeanVMCircuits.Flock.adder64_soundness,
+    ``LeanVMCircuits.Flock.adder64_wellFormed, ``LeanVMCircuits.Flock.adder64_complete,
+    ``LeanVMCircuits.Flock.adder32_source, ``LeanVMCircuits.Flock.adder32_soundness,
+    ``LeanVMCircuits.Flock.adder32_layout, ``LeanVMCircuits.Flock.adder32_wellFormed,
+    ``LeanVMCircuits.Flock.adder32_complete, ``LeanVMCircuits.Flock.carryAdder64_source,
+    ``LeanVMCircuits.Flock.carryAdder64_soundness, ``LeanVMCircuits.Flock.carryAdder64_layout,
+    ``LeanVMCircuits.Flock.carryAdder64_wellFormed, ``LeanVMCircuits.Flock.carryAdder64_complete,
+    ``LeanVMCircuits.Flock.lookup_rejected, ``LeanVMCircuits.Flock.interaction_rejected] do
+    let axioms ← collectAxioms theoremName
+    for axiomName in axioms do
+      unless #[``propext, ``Classical.choice, ``Quot.sound].contains axiomName do
+        throwError "{theoremName} depends on unexpected axiom {axiomName}"
diff --git a/verification/circuits/Generate.lean b/verification/circuits/Generate.lean
new file mode 100644
index 000000000..b318f925f
--- /dev/null
+++ b/verification/circuits/Generate.lean
@@ -0,0 +1,76 @@
+import LeanVMCircuits.AdderFamily
+
+open LeanVMCircuits.Flock
+
+structure Codegen where
+  bindings : List (Nat × String)
+  cache : List (Affine × String) := []
+  lines : Array String := #[]
+  next : Nat := 0
+
+def fresh (state : Codegen) (operation : String) : String × Codegen :=
+  let name := s!"w{state.next}"
+  (name, { state with next := state.next + 1, lines := state.lines.push s!"    let {name} = {operation};" })
+
+def emitAffine (affine : Affine) (state : Codegen) : Except String (String × Codegen) :=
+  if let some name := state.cache.findSome? (fun (key, name) => if key = affine then some name else none) then
+    .ok (name, state)
+  else
+    match affine with
+    | .zero => .ok ("Wire::ZERO", state)
+    | .one => .ok ("Wire::ONE", state)
+    | .var index =>
+      match state.bindings.findSome? (fun (key, name) => if key = index then some name else none) with
+      | some name => .ok (name, state)
+      | none => .error s!"unbound or forward variable {index}"
+    | .xor left right => do
+      let (leftName, state) ← emitAffine left state
+      let (rightName, state) ← emitAffine right state
+      let (name, state) := fresh state s!"c.xor({leftName}, {rightName})"
+      return (name, { state with cache := (affine, name) :: state.cache })
+
+def emit (name : String) (width : Nat) (withCarry : Bool) (artifact : Artifact) : Except String String := do
+  let bindings := (List.range width).flatMap fun i => [(i, s!"x[{i}]"), (width + i, s!"y[{i}]")]
+  let bindings := if withCarry then (2 * width, "carry_in") :: bindings else bindings
+  let mut state : Codegen := { bindings }
+  for row in artifact.rows do
+    if state.bindings.any (fun (index, _) => index == row.output) then
+      throw s!"duplicate product variable {row.output}"
+    let (left, afterLeft) ← emitAffine row.left state
+    let (right, afterRight) ← emitAffine row.right afterLeft
+    let (name, afterProduct) := fresh afterRight s!"c.and({left}, {right})"
+    state := { afterProduct with bindings := (row.output, name) :: afterProduct.bindings }
+  let mut outputs : Array String := #[]
+  for affine in artifact.outputs do
+    let (name, afterOutput) ← emitAffine affine state
+    state := afterOutput
+    outputs := outputs.push name
+  if outputs.size != width + (if withCarry then 1 else 0) then throw "unexpected exported output width"
+  let parameter := if withCarry then ", carry_in: Wire" else ""
+  let result := if withCarry then s!"([Wire; {width}], Wire)" else s!"[Wire; {width}]"
+  let header := s!"/// The checked {name} artifact, least-significant-bit products first.\n\
+    pub fn {name}(c: &mut Builder, x: &[Wire; {width}], y: &[Wire; {width}]{parameter}) -> {result} \{\n"
+  let outputLines := (List.range (width / 4)).map fun line =>
+    "        " ++ String.intercalate ", " ((List.range 4).map fun i => outputs[line * 4 + i]!) ++ ","
+  let opening := if withCarry then "\n    (\n    [\n" else "\n    [\n"
+  let closing := if withCarry then s!"\n    ],\n    {outputs[width]!},\n    )\n}\n" else "\n    ]\n}\n"
+  return header ++ String.intercalate "\n" state.lines.toList ++ opening ++
+    String.intercalate "\n" outputLines ++ closing
+
+def emitProduction : Except String String := do
+  let wrapping64 ← emit "wrapping_add64" 64 false adder64
+  let wrapping32 ← emit "wrapping_add32" 32 false adder32
+  let carry64 ← emit "add_with_carry64" 64 true carryAdder64
+  return "// Generated by verification/circuits/Generate.lean from checked Flock artifacts. Do not edit.\n\
+    //! Clean-authored GF(2) circuits consumed by production instruction classes.\n\n\
+    use crate::circuit::{Builder, Wire};\n\n" ++ wrapping64 ++ "\n" ++ wrapping32 ++ "\n" ++ carry64
+
+def main (args : List String) : IO Unit := do
+  let [destination] := args | throw (IO.userError "usage: lake env lean --run Generate.lean <destination.rs>")
+  match emitProduction with
+  | .error message => throw (IO.userError message)
+  | .ok code =>
+    IO.FS.writeFile destination code
+    let format ← IO.Process.output {
+      cmd := "rustfmt", args := #["--config-path", "../../rustfmt.toml", destination] }
+    if format.exitCode != 0 then throw (IO.userError format.stderr)
diff --git a/verification/circuits/LeanVMCircuits.lean b/verification/circuits/LeanVMCircuits.lean
new file mode 100644
index 000000000..377cf2e30
--- /dev/null
+++ b/verification/circuits/LeanVMCircuits.lean
@@ -0,0 +1,3 @@
+module
+
+public import LeanVMCircuits.AdderFamily
diff --git a/verification/circuits/LeanVMCircuits/Adder.lean b/verification/circuits/LeanVMCircuits/Adder.lean
new file mode 100644
index 000000000..9586c6a6f
--- /dev/null
+++ b/verification/circuits/LeanVMCircuits/Adder.lean
@@ -0,0 +1,258 @@
+module
+
+public import Clean.Circuit.Subcircuit
+public import Clean.Utils.Tactics
+public import Clean.Utils.Tactics.ProvableStructDeriving
+public import Mathlib.Tactic
+
+@[expose] public section
+
+namespace LeanVMCircuits
+
+abbrev Bit := F 2
+
+instance : Fact (Nat.Prime 2) := ⟨by decide⟩
+
+namespace FullAdder
+
+structure Input (F : Type) where
+  x : F
+  y : F
+  carry : F
+  deriving ProvableStruct
+
+structure Output (F : Type) where
+  sum : F
+  carry : F
+  deriving ProvableStruct
+
+/-- One GF(2) product implements majority; the sum is affine. -/
+def main (input : Var Input Bit) : Circuit Bit (Var Output Bit) := do
+  let xc := input.x + input.carry
+  let yc := input.y + input.carry
+  let product ← witness (xc * yc)
+  assertZero (product - xc * yc)
+  return { sum := xc + input.y, carry := product + input.carry }
+
+/-- Independent integer addition of three bits, including the carry out. -/
+def Spec (input : Input Bit) (output : Output Bit) : Prop :=
+  output.sum.val + 2 * output.carry.val = input.x.val + input.y.val + input.carry.val
+
+instance elaborated : ElaboratedCircuit Bit Input Output main := by
+  elaborate_circuit
+
+theorem bit_addition (x y c : Bit) :
+    (x + c + y).val + 2 * ((x + c) * (y + c) + c).val = x.val + y.val + c.val := by
+  have hx := ZMod.val_lt x
+  have hy := ZMod.val_lt y
+  have hc := ZMod.val_lt c
+  have ex : x = (x.val : Bit) := (ZMod.natCast_zmod_val x).symm
+  have ey : y = (y.val : Bit) := (ZMod.natCast_zmod_val y).symm
+  have ec : c = (c.val : Bit) := (ZMod.natCast_zmod_val c).symm
+  interval_cases hxx : x.val <;> interval_cases hyy : y.val <;> interval_cases hcc : c.val <;>
+    simp_all <;> decide
+
+theorem soundness : Soundness Bit main (fun _ => True) Spec := by
+  circuit_proof_start
+  rcases h_input with ⟨hx, hy, hc⟩
+  rw [sub_eq_zero] at h_holds
+  rw [h_holds]
+  exact bit_addition _ _ _
+
+theorem completeness : Completeness Bit main (fun _ => True) := by
+  circuit_proof_start
+  simp_all
+
+@[circuit_norm]
+def circuit : FormalCircuit Bit Input Output where
+  main
+  elaborated
+  Spec
+  soundness
+  completeness
+
+end FullAdder
+
+namespace Adder
+
+structure Input (n : ℕ) (F : Type) where
+  x : Vector F n
+  y : Vector F n
+  carry : F
+  deriving ProvableStruct
+
+structure Output (n : ℕ) (F : Type) where
+  sum : Vector F n
+  carry : F
+  deriving ProvableStruct
+
+/-- Little-endian unsigned interpretation, independent of circuit constraints. -/
+def value {n : ℕ} (bits : Vector Bit n) : ℕ :=
+  bits.toList.foldr (fun b acc => b.val + 2 * acc) 0
+
+theorem value_push {n : ℕ} (bits : Vector Bit n) (b : Bit) :
+    value (bits.push b) = value bits + 2 ^ n * b.val := by
+  induction bits using Vector.induct with
+  | nil => simp [value]
+  | @cons n head tail ih =>
+    rw [Vector.listCons_push]
+    simp only [value, Vector.toList_listCons, List.foldr_cons] at *
+    rw [ih, pow_succ]
+    ring
+
+theorem value_zero (bits : Vector Bit 0) : value bits = 0 := by
+  have h : bits = #v[] := by ext i hi; omega
+  simp [h, value]
+
+theorem value_pop {n : ℕ} (bits : Vector Bit (n + 1)) :
+    value bits = value bits.pop + 2 ^ n * bits[n].val := by
+  have h := value_push bits.pop bits.back
+  rw [Vector.push_pop_back, Vector.back_eq_getElem] at h
+  exact h
+
+theorem value_lt {n : ℕ} (bits : Vector Bit n) : value bits < 2 ^ n := by
+  induction bits using Vector.induct with
+  | nil => simp [value]
+  | @cons n head tail ih =>
+    have hbit := ZMod.val_lt head
+    simp only [value, Vector.toList_listCons, List.foldr_cons, pow_succ] at *
+    omega
+
+def Spec (n : ℕ) (input : Input n Bit) (output : Output n Bit) : Prop :=
+  value output.sum + 2 ^ n * output.carry.val = value input.x + value input.y + input.carry.val
+
+/-- Metadata invariants keep recursive subcircuit specifications opaque to Clean's elaborator. -/
+structure Certified (n : ℕ) where
+  circuit : FormalCircuit Bit (Input n) (Output n)
+  assumptions_eq : circuit.Assumptions = fun _ => True
+  spec_eq : circuit.Spec = Spec n
+  requirements_eq : circuit.channelsWithRequirements = []
+  guarantees_eq : circuit.elaborated.channelsWithGuarantees = []
+
+def zero : Certified 0 where
+  circuit := {
+    main := fun input => pure { sum := #v[], carry := input.carry }
+    Spec := Spec 0
+    soundness := by
+      circuit_proof_start
+      simp_all [value_zero, circuit_norm]
+    completeness := by circuit_proof_start
+  }
+  assumptions_eq := rfl
+  spec_eq := rfl
+  requirements_eq := rfl
+  guarantees_eq := rfl
+
+def step (n : ℕ) (previous : Certified n) : Certified (n + 1) where
+  circuit := {
+    main := fun input => do
+      let lower ← previous.circuit { x := input.x.pop, y := input.y.pop, carry := input.carry }
+      let upper ← FullAdder.circuit { x := input.x[n], y := input.y[n], carry := lower.carry }
+      return { sum := lower.sum.push upper.sum, carry := upper.carry }
+    Spec := Spec (n + 1)
+    requirementsChannelsLawful := by
+      simp only [circuit_norm, previous.requirements_eq]
+    soundness := by
+      circuit_proof_start [FullAdder.circuit, FullAdder.Spec]
+      simp only [previous.assumptions_eq, previous.spec_eq,
+        previous.requirements_eq, true_implies, or_true] at *
+      simp only [Spec, FormalCircuitBase.output, ← ElaboratedCircuit.output_eq] at h_holds ⊢
+      generalize hlow : (previous.circuit.main
+        { x := input_var_x.pop, y := input_var_y.pop, carry := input_var_carry }).output i₀ = low at *
+      rcases low with ⟨ls, lc⟩
+      provable_struct_simp
+      simp only [Vector.map_push, value_push, circuit_norm] at h_holds ⊢
+      rcases h_input with ⟨hx, hy, hc⟩
+      have hxbit := congrArg (fun v : Vector Bit (n + 1) => v[n]) hx
+      have hybit := congrArg (fun v : Vector Bit (n + 1) => v[n]) hy
+      simp only [Vector.getElem_map] at hxbit hybit
+      simp only [hxbit, hybit, Vector.map_pop, hx, hy] at h_holds ⊢
+      rw [value_pop input_x, value_pop input_y, pow_succ]
+      rcases h_holds with ⟨hlower, hupper⟩
+      simp only [FormalCircuitBase.localLength,
+        ← ElaboratedCircuit.localLength_eq (offset := 0)] at hupper ⊢
+      nlinarith [congrArg (fun v : ℕ => 2 ^ n * v) hupper]
+    completeness := by
+      circuit_proof_start [FullAdder.circuit, FullAdder.Spec]
+      simp [previous.assumptions_eq]
+  }
+  assumptions_eq := rfl
+  spec_eq := rfl
+  requirements_eq := rfl
+  guarantees_eq := by
+    simp only [circuit_norm, previous.guarantees_eq]
+
+/-- Clean composes certified one-bit adders in least-significant-bit product order. -/
+def certified : (n : ℕ) → Certified n
+  | 0 => zero
+  | n + 1 => step n (certified n)
+
+def circuit (n : ℕ) := (certified n).circuit
+
+@[circuit_norm] theorem circuit_assumptions (n : ℕ) :
+    (circuit n).Assumptions = fun _ => True := (certified n).assumptions_eq
+@[circuit_norm] theorem circuit_spec (n : ℕ) :
+    (circuit n).Spec = Spec n := (certified n).spec_eq
+@[circuit_norm] theorem circuit_requirements (n : ℕ) :
+    (circuit n).channelsWithRequirements = [] := (certified n).requirements_eq
+@[circuit_norm] theorem circuit_guarantees (n : ℕ) :
+    (circuit n).elaborated.channelsWithGuarantees = [] := (certified n).guarantees_eq
+
+end Adder
+
+namespace WrappingAdder
+
+structure Input (n : ℕ) (F : Type) where
+  x : Vector F n
+  y : Vector F n
+  deriving ProvableStruct
+
+/-- The final sum is affine. The discarded overflow has no witness or product slot. -/
+def main (n : ℕ) (input : Var (Input (n + 1)) Bit) : Circuit Bit (Var (fields (n + 1)) Bit) := do
+  let lower ← Adder.circuit n { x := input.x.pop, y := input.y.pop, carry := 0 }
+  return lower.sum.push (input.x[n] + lower.carry + input.y[n])
+
+def Spec (n : ℕ) (input : Input (n + 1) Bit) (output : Vector Bit (n + 1)) : Prop :=
+  Adder.value output = (Adder.value input.x + Adder.value input.y) % 2 ^ (n + 1)
+
+theorem wrapping_value {n : ℕ} (x y : Vector Bit (n + 1)) (sum : Vector Bit n) (carry : Bit)
+    (h : Adder.value sum + 2 ^ n * carry.val = Adder.value x.pop + Adder.value y.pop) :
+    Adder.value (sum.push (x[n] + carry + y[n])) =
+      (Adder.value x + Adder.value y) % 2 ^ (n + 1) := by
+  have hupper := FullAdder.bit_addition x[n] y[n] carry
+  have htotal : Adder.value x + Adder.value y =
+      Adder.value (sum.push (x[n] + carry + y[n])) +
+        ((x[n] + carry) * (y[n] + carry) + carry).val * 2 ^ (n + 1) := by
+    rw [Adder.value_pop x, Adder.value_pop y, Adder.value_push, pow_succ]
+    nlinarith [congrArg (fun v : ℕ => 2 ^ n * v) hupper]
+  rw [htotal]
+  simp [Nat.add_mod, Nat.mod_eq_of_lt (Adder.value_lt _)]
+
+def circuit (n : ℕ) : FormalCircuit Bit (Input (n + 1)) (fields (n + 1)) where
+  main := main n
+  Spec := Spec n
+  soundness := by
+    circuit_proof_start
+    simp only [Adder.Spec, circuit_norm] at h_holds
+    simp only [FormalCircuitBase.output, ← ElaboratedCircuit.output_eq] at h_holds ⊢
+    generalize hlow : ((Adder.circuit n).main
+      { x := input_var_x.pop, y := input_var_y.pop, carry := 0 }).output i₀ = low at *
+    rcases low with ⟨ls, lc⟩
+    provable_struct_simp
+    simp only [Vector.map_push, circuit_norm] at h_holds ⊢
+    rcases h_input with ⟨hx, hy⟩
+    have hxbit := congrArg (fun v : Vector Bit (n + 1) => v[n]) hx
+    have hybit := congrArg (fun v : Vector Bit (n + 1) => v[n]) hy
+    simp only [Vector.getElem_map] at hxbit hybit
+    simp only [hxbit, hybit, Vector.map_pop, hx, hy, circuit_norm] at h_holds ⊢
+    simp only [Adder.circuit, Circuit.output] at hlow
+    simp only [hlow, circuit_norm] at ⊢
+    simp only [ZMod.val_zero, add_zero] at h_holds
+    exact wrapping_value _ _ _ _ h_holds
+  completeness := by circuit_proof_start
+
+/-- The production doubleword memory-address circuit. -/
+def adder64 := circuit 63
+
+end WrappingAdder
+end LeanVMCircuits
diff --git a/verification/circuits/LeanVMCircuits/AdderFamily.lean b/verification/circuits/LeanVMCircuits/AdderFamily.lean
new file mode 100644
index 000000000..302f73ccc
--- /dev/null
+++ b/verification/circuits/LeanVMCircuits/AdderFamily.lean
@@ -0,0 +1,88 @@
+module
+
+public import LeanVMCircuits.Completeness
+
+@[expose] public section
+
+namespace LeanVMCircuits.Flock
+
+def adder32 : Artifact := checked (lowerCircuit 31) (by decide +kernel)
+
+theorem adder32_source : lowerCircuit 31 = .ok adder32 := checked_eq _ _
+
+theorem adder32_soundness (env : Environment Bit)
+    (hrows : adder32.rows.Forall (Row.Holds env.get)) :
+    adder32.value env.get =
+      (Adder.value ((inputs 31).x.map (Expression.eval env)) +
+        Adder.value ((inputs 31).y.map (Expression.eval env))) % 2 ^ 32 :=
+  exported_soundness 31 adder32 adder32_source env hrows
+
+theorem adder32_layout :
+    adder32.rows.map Row.output = (List.range 31).map (64 + ·) ∧ adder32.outputs.length = 32 := by
+  decide +kernel
+
+theorem adder32_wellFormed : wellFormed 64 adder32.rows = true := by decide +kernel
+
+theorem adder32_complete (inputs : ℕ → Bit) :
+    ∃ assignment, AgreeBelow 64 inputs assignment ∧ adder32.rows.Forall (Row.Holds assignment) :=
+  witness_exists adder32.rows 64 inputs adder32_wellFormed
+
+def carryInputs (n : ℕ) : Var (Adder.Input n) Bit :=
+  { x := Vector.mapRange n fun i => var ⟨i⟩,
+    y := Vector.mapRange n fun i => var ⟨n + i⟩,
+    carry := var ⟨2 * n⟩ }
+
+def carrySource (n : ℕ) := (Adder.circuit n).toSubcircuit (2 * n + 1) (carryInputs n)
+
+def carryOutput (n : ℕ) : Vector (Expression Bit) (n + 1) :=
+  let output := (Adder.circuit n).output (carryInputs n) (2 * n + 1)
+  output.sum.push output.carry
+
+def lowerCarry (n : ℕ) : Except String Artifact :=
+  lowerAt (carrySource n).ops (carryOutput n).toList
+
+theorem carry_exported_soundness (n : ℕ) (artifact : Artifact)
+    (hcode : lowerCarry n = .ok artifact) (env : Environment Bit)
+    (hrows : artifact.rows.Forall (Row.Holds env.get)) :
+    artifact.value env.get = Adder.value ((carryInputs n).x.map (Expression.eval env)) +
+      Adder.value ((carryInputs n).y.map (Expression.eval env)) + (env.get (2 * n)).val := by
+  have h := lowerAt_correct _ _ artifact hcode env
+  have hassumptions : (carrySource n).Assumptions env := by
+    change (Adder.circuit n).Assumptions (eval env (carryInputs n))
+    rw [Adder.circuit_assumptions]
+    trivial
+  have hspec := ((carrySource n).soundness env hassumptions (h.1.mp hrows) h.2.1).1
+  change (Adder.circuit n).Spec (eval env (carryInputs n))
+    (eval env ((Adder.circuit n).output (carryInputs n) (2 * n + 1))) at hspec
+  rw [Adder.circuit_spec] at hspec
+  dsimp [Artifact.value]
+  rw [← List.foldr_map (f := Affine.eval env.get) (g := fun b acc => b.val + 2 * acc), h.2.2,
+    ← Vector.toList_map]
+  change Adder.value ((carryOutput n).map (Expression.eval env)) = _
+  rw [carryOutput, Vector.map_push, Adder.value_push]
+  generalize hout : (Adder.circuit n).output (carryInputs n) (2 * n + 1) = output at *
+  rcases output with ⟨sum, carry⟩
+  provable_struct_simp
+  simpa only [Adder.Spec, carryInputs, circuit_norm] using hspec
+
+def carryAdder64 : Artifact := checked (lowerCarry 64) (by decide +kernel)
+
+theorem carryAdder64_source : lowerCarry 64 = .ok carryAdder64 := checked_eq _ _
+
+theorem carryAdder64_soundness (env : Environment Bit)
+    (hrows : carryAdder64.rows.Forall (Row.Holds env.get)) :
+    carryAdder64.value env.get = Adder.value ((carryInputs 64).x.map (Expression.eval env)) +
+      Adder.value ((carryInputs 64).y.map (Expression.eval env)) + (env.get 128).val :=
+  carry_exported_soundness 64 carryAdder64 carryAdder64_source env hrows
+
+theorem carryAdder64_layout :
+    carryAdder64.rows.map Row.output = (List.range 64).map (129 + ·) ∧
+      carryAdder64.outputs.length = 65 := by decide +kernel
+
+theorem carryAdder64_wellFormed : wellFormed 129 carryAdder64.rows = true := by decide +kernel
+
+theorem carryAdder64_complete (inputs : ℕ → Bit) :
+    ∃ assignment, AgreeBelow 129 inputs assignment ∧ carryAdder64.rows.Forall (Row.Holds assignment) :=
+  witness_exists carryAdder64.rows 129 inputs carryAdder64_wellFormed
+
+end LeanVMCircuits.Flock
diff --git a/verification/circuits/LeanVMCircuits/Completeness.lean b/verification/circuits/LeanVMCircuits/Completeness.lean
new file mode 100644
index 000000000..fcf3bc91d
--- /dev/null
+++ b/verification/circuits/LeanVMCircuits/Completeness.lean
@@ -0,0 +1,65 @@
+module
+
+public import LeanVMCircuits.Export
+
+@[expose] public section
+
+namespace LeanVMCircuits.Flock
+
+/-- All variable references precede the product they help generate. -/
+def Affine.bounded (affine : Affine) (limit : ℕ) : Bool :=
+  match affine with
+  | .zero | .one => true
+  | .var index => decide (index < limit)
+  | .xor left right => left.bounded limit && right.bounded limit
+
+def AgreeBelow (limit : ℕ) (before after : ℕ → Bit) : Prop :=
+  ∀ index, index < limit → after index = before index
+
+theorem Affine.eval_agree (affine : Affine) (limit : ℕ) (before after : ℕ → Bit)
+    (hbound : affine.bounded limit = true) (hagree : AgreeBelow limit before after) :
+    affine.eval after = affine.eval before := by
+  induction affine with
+  | zero => rfl
+  | one => rfl
+  | var index => exact hagree index (by simpa [Affine.bounded] using hbound)
+  | xor left right ihLeft ihRight =>
+    simp only [Affine.bounded, Bool.and_eq_true] at hbound
+    exact congrArg₂ (· + ·) (ihLeft hbound.1) (ihRight hbound.2)
+
+def wellFormed (next : ℕ) : List Row → Bool
+  | [] => true
+  | row :: rest => row.output == next && row.left.bounded next && row.right.bounded next &&
+      wellFormed (next + 1) rest
+
+/-- Every input assignment extends to a satisfying assignment, not just a conditional witness premise. -/
+theorem witness_exists (rows : List Row) (next : ℕ) (assignment : ℕ → Bit)
+    (hwell : wellFormed next rows = true) :
+    ∃ final, AgreeBelow next assignment final ∧ rows.Forall (Row.Holds final) := by
+  induction rows generalizing next assignment with
+  | nil => exact ⟨assignment, fun _ _ => rfl, by simp⟩
+  | cons row rest ih =>
+    simp only [wellFormed, Bool.and_eq_true, Nat.beq_eq_true_eq] at hwell
+    rcases hwell with ⟨⟨⟨houtput, hleft⟩, hright⟩, hrest⟩
+    let updated := Function.update assignment next (row.left.eval assignment * row.right.eval assignment)
+    obtain ⟨final, hagree, htail⟩ := ih (next + 1) updated hrest
+    have htotal : AgreeBelow next assignment final := by
+      intro index hindex
+      rw [hagree index (by omega)]
+      exact Function.update_of_ne (by omega) _ _
+    refine ⟨final, htotal, ?_⟩
+    simp only [List.forall_cons]
+    refine ⟨?_, htail⟩
+    change final row.output = row.left.eval final * row.right.eval final
+    rw [Affine.eval_agree row.left next assignment final hleft htotal,
+      Affine.eval_agree row.right next assignment final hright htotal, houtput,
+      hagree next (by omega)]
+    simp [updated]
+
+theorem adder64_wellFormed : wellFormed 128 adder64.rows = true := by decide +kernel
+
+theorem adder64_complete (inputs : ℕ → Bit) :
+    ∃ assignment, AgreeBelow 128 inputs assignment ∧ adder64.rows.Forall (Row.Holds assignment) :=
+  witness_exists adder64.rows 128 inputs adder64_wellFormed
+
+end LeanVMCircuits.Flock
diff --git a/verification/circuits/LeanVMCircuits/Export.lean b/verification/circuits/LeanVMCircuits/Export.lean
new file mode 100644
index 000000000..54845af02
--- /dev/null
+++ b/verification/circuits/LeanVMCircuits/Export.lean
@@ -0,0 +1,124 @@
+module
+
+public import LeanVMCircuits.Flatten
+
+@[expose] public section
+
+namespace LeanVMCircuits.Flock
+
+structure Artifact where
+  rows : List Row
+  outputs : List Affine
+  deriving Repr, DecidableEq
+
+def lowerOutputs : List (Expression Bit) → Except String (List Affine)
+  | [] => .ok []
+  | expression :: rest =>
+    match lowerAffine expression, lowerOutputs rest with
+    | .ok affine, .ok affines => .ok (affine :: affines)
+    | .error message, _ => .error message
+    | _, .error message => .error message
+
+theorem lowerOutputs_correct (expressions : List (Expression Bit)) (affines : List Affine)
+    (h : lowerOutputs expressions = .ok affines) (env : Environment Bit) :
+    affines.map (Affine.eval env.get) = expressions.map (Expression.eval env) := by
+  induction expressions generalizing affines with
+  | nil => simp [lowerOutputs] at h; subst affines; rfl
+  | cons expression rest ih =>
+    cases ha : lowerAffine expression with
+    | error message => simp [lowerOutputs, ha] at h
+    | ok affine =>
+      cases hr : lowerOutputs rest with
+      | error message => simp [lowerOutputs, ha, hr] at h
+      | ok tail =>
+        simp [lowerOutputs, ha, hr] at h
+        subst affines
+        simp only [List.map_cons, lowerAffine_correct _ _ ha env, ih _ hr]
+
+def inputs (n : ℕ) : Var (WrappingAdder.Input (n + 1)) Bit :=
+  { x := Vector.mapRange (n + 1) fun i => var ⟨i⟩,
+    y := Vector.mapRange (n + 1) fun i => var ⟨n + 1 + i⟩ }
+
+def source (n : ℕ) := (WrappingAdder.circuit n).toSubcircuit (2 * (n + 1)) (inputs n)
+
+def lowerAt (nested : NestedOperations Bit) (output : List (Expression Bit)) : Except String Artifact :=
+  match flatten 128 nested with
+  | .error message => .error message
+  | .ok operations =>
+    match lower operations, lowerOutputs output with
+    | .ok rows, .ok outputs => .ok { rows, outputs }
+    | .error message, _ => .error message
+    | _, .error message => .error message
+
+def lowerCircuit (n : ℕ) : Except String Artifact :=
+  lowerAt (source n).ops ((WrappingAdder.circuit n).output (inputs n) (2 * (n + 1))).toList
+
+def checked {α : Type} (result : Except String α) (h : result.isOk = true) : α :=
+  match result with
+  | .ok value => value
+  | .error _ => False.elim (by simp only [Except.isOk, Except.toBool, Bool.false_eq_true] at h)
+
+theorem checked_eq {α : Type} (result : Except String α) (h : result.isOk = true) :
+    result = .ok (checked result h) := by
+  cases result with
+  | ok value => rfl
+  | error message => simp only [Except.isOk, Except.toBool, Bool.false_eq_true] at h
+
+/-- Checked by reduction in Lean's kernel, not by a native-decision axiom. -/
+theorem export64_supported : (lowerCircuit 63).isOk = true := by decide +kernel
+
+def adder64 : Artifact := checked (lowerCircuit 63) export64_supported
+
+theorem adder64_source : lowerCircuit 63 = .ok adder64 := checked_eq _ _
+
+def Artifact.value (artifact : Artifact) (assignment : ℕ → Bit) : ℕ :=
+  artifact.outputs.foldr (fun wire acc => (wire.eval assignment).val + 2 * acc) 0
+
+theorem lowerAt_correct (nested : NestedOperations Bit) (output : List (Expression Bit))
+    (artifact : Artifact) (hcode : lowerAt nested output = .ok artifact) (env : Environment Bit) :
+    (artifact.rows.Forall (Row.Holds env.get) ↔ ConstraintsHoldFlat env nested.toFlat) ∧
+      FlatOperation.Guarantees env nested.toFlat ∧
+      artifact.outputs.map (Affine.eval env.get) = output.map (Expression.eval env) := by
+  cases hf : flatten 128 nested with
+  | error message => simp [lowerAt, hf] at hcode
+  | ok operations =>
+    cases hr : lower operations with
+    | error message => simp [lowerAt, hf, hr] at hcode
+    | ok rows =>
+      cases ho : lowerOutputs output with
+      | error message => simp [lowerAt, hf, hr, ho] at hcode
+      | ok outputs =>
+        simp [lowerAt, hf, hr, ho] at hcode
+        subst artifact
+        rw [← flatten_correct _ _ _ hf]
+        refine ⟨lower_correct operations rows hr env, ?_, lowerOutputs_correct _ _ ho env⟩
+        rw [FlatOperation.guarantees_iff_forall_mem, lower_no_interactions _ _ hr]
+        simp
+
+/-- Successful export preserves arbitrary-witness soundness of the exact Clean source. -/
+theorem exported_soundness (n : ℕ) (artifact : Artifact)
+    (hcode : lowerCircuit n = .ok artifact) (env : Environment Bit)
+    (hrows : artifact.rows.Forall (Row.Holds env.get)) :
+    artifact.value env.get =
+      (Adder.value ((inputs n).x.map (Expression.eval env)) +
+        Adder.value ((inputs n).y.map (Expression.eval env))) % 2 ^ (n + 1) := by
+  have h := lowerAt_correct _ _ artifact hcode env
+  have hspec := ((source n).soundness env (by change True; trivial) (h.1.mp hrows) h.2.1).1
+  change WrappingAdder.Spec n (eval env (inputs n))
+    (eval env ((WrappingAdder.circuit n).output (inputs n) (2 * (n + 1)))) at hspec
+  dsimp [Artifact.value, WrappingAdder.Spec, Adder.value] at hspec ⊢
+  rw [← List.foldr_map (f := Affine.eval env.get) (g := fun b acc => b.val + 2 * acc), h.2.2]
+  simpa only [inputs, circuit_norm, Vector.toList_map] using hspec
+
+theorem adder64_soundness (env : Environment Bit)
+    (hrows : adder64.rows.Forall (Row.Holds env.get)) :
+    adder64.value env.get =
+      (Adder.value ((inputs 63).x.map (Expression.eval env)) +
+        Adder.value ((inputs 63).y.map (Expression.eval env))) % 2 ^ 64 :=
+  exported_soundness 63 adder64 adder64_source env hrows
+
+theorem adder64_layout :
+    adder64.rows.map Row.output = (List.range 63).map (128 + ·) ∧
+      adder64.outputs.length = 64 := by decide +kernel
+
+end LeanVMCircuits.Flock
diff --git a/verification/circuits/LeanVMCircuits/Flatten.lean b/verification/circuits/LeanVMCircuits/Flatten.lean
new file mode 100644
index 000000000..74000f270
--- /dev/null
+++ b/verification/circuits/LeanVMCircuits/Flatten.lean
@@ -0,0 +1,57 @@
+module
+
+public import LeanVMCircuits.Lowering
+
+@[expose] public section
+
+namespace LeanVMCircuits.Flock
+
+def concatenate {α : Type} : List (Except String (List α)) → Except String (List α)
+  | [] => .ok []
+  | .error message :: _ => .error message
+  | .ok head :: tail =>
+    match concatenate tail with
+    | .error message => .error message
+    | .ok rest => .ok (head ++ rest)
+
+/-- A bounded, kernel-computable flattening of Clean subcircuits. Excess nesting is an error. -/
+def flatten : ℕ → NestedOperations Bit → Except String (List (FlatOperation Bit))
+  | 0, _ => .error "Flock export exceeds the supported subcircuit nesting depth"
+  | _ + 1, .single operation => .ok [operation]
+  | depth + 1, .nested (_, children) => concatenate (children.map (flatten depth))
+
+private theorem concatenate_correct {α β : Type} (xs : List α)
+    (f : α → Except String (List β)) (g : α → List β)
+    (hfg : ∀ x ∈ xs, ∀ result, f x = .ok result → result = g x)
+    (result : List β) (h : concatenate (xs.map f) = .ok result) :
+    result = xs.flatMap g := by
+  induction xs generalizing result with
+  | nil => simp [concatenate] at h; subst result; rfl
+  | cons x xs ih =>
+    cases hx : f x with
+    | error message => simp [concatenate, hx] at h
+    | ok head =>
+      cases ht : concatenate (xs.map f) with
+      | error message => simp [concatenate, hx, ht] at h
+      | ok tail =>
+        simp [concatenate, hx, ht] at h
+        subst result
+        rw [hfg x (by simp) head hx, ih (fun x hmem => hfg x (by simp [hmem])) tail ht]
+        rfl
+
+/-- The bounded flattener agrees with Clean's actual nested semantics whenever it succeeds. -/
+theorem flatten_correct (depth : ℕ) (nested : NestedOperations Bit)
+    (operations : List (FlatOperation Bit)) (h : flatten depth nested = .ok operations) :
+    operations = nested.toFlat := by
+  induction depth generalizing nested operations with
+  | zero => simp [flatten] at h
+  | succ depth ih =>
+    cases nested with
+    | single operation => simpa only [flatten, NestedOperations.toFlat, Except.ok.injEq] using h.symm
+    | nested pair =>
+      rcases pair with ⟨name, children⟩
+      simp only [flatten, NestedOperations.toFlat] at h ⊢
+      exact concatenate_correct children (flatten depth) NestedOperations.toFlat
+        (fun child _ result hchild => ih child result hchild) operations h
+
+end LeanVMCircuits.Flock
diff --git a/verification/circuits/LeanVMCircuits/Lowering.lean b/verification/circuits/LeanVMCircuits/Lowering.lean
new file mode 100644
index 000000000..cf6e76e6d
--- /dev/null
+++ b/verification/circuits/LeanVMCircuits/Lowering.lean
@@ -0,0 +1,119 @@
+module
+
+public import LeanVMCircuits.Adder
+
+@[expose] public section
+
+namespace LeanVMCircuits.Flock
+
+-- Clean's generic equality transports through `propext`; use GF(2)'s computable representation here.
+local instance : DecidableEq Bit := inferInstanceAs (DecidableEq (Fin 2))
+
+/-- Flock's free affine wires. Product variables are committed row slots. -/
+inductive Affine where
+  | zero
+  | one
+  | var (index : ℕ)
+  | xor (left right : Affine)
+  deriving Repr, DecidableEq
+
+def Affine.eval (assignment : ℕ → Bit) : Affine → Bit
+  | .zero => 0
+  | .one => 1
+  | .var i => assignment i
+  | .xor a b => a.eval assignment + b.eval assignment
+
+/-- One committed product, in exactly the source order. -/
+structure Row where
+  output : ℕ
+  left : Affine
+  right : Affine
+  deriving Repr, DecidableEq
+
+def Row.Holds (assignment : ℕ → Bit) (row : Row) : Prop :=
+  assignment row.output = row.left.eval assignment * row.right.eval assignment
+
+/-- Only affine operands are supported; no multiplication is silently expanded. -/
+def lowerAffine : Expression Bit → Except String Affine
+  | .var v => .ok (.var v.index)
+  | .const c => if c = 0 then .ok .zero else if c = 1 then .ok .one else .error "unsupported constant"
+  | .add a b =>
+    match lowerAffine a, lowerAffine b with
+    | .ok left, .ok right => .ok (.xor left right)
+    | .error message, _ => .error message
+    | _, .error message => .error message
+  | .mul _ _ => .error "non-affine product operand"
+
+/-- A scalar witness followed by its defining product assertion is the supported operation pair. -/
+def lower : List (FlatOperation Bit) → Except String (List Row)
+  | [] => .ok []
+  | .witness 1 _ :: .assert (.add (.var output) (.mul (.const coefficient) (.mul a b))) :: rest =>
+    if coefficient = -1 then
+      match lowerAffine a with
+      | .error message => .error message
+      | .ok left =>
+        match lowerAffine b with
+        | .error message => .error message
+        | .ok right =>
+          match lower rest with
+          | .error message => .error message
+          | .ok rows => .ok ({ output := output.index, left, right } :: rows)
+    else .error "product assertion must subtract its right-hand side"
+  | .witness _ _ :: _ => .error "unsupported witness or missing product assertion"
+  | .assert _ :: _ => .error "unsupported assertion"
+  | .lookup _ :: _ => .error "Flock lowering does not support lookups"
+  | .interact _ :: _ => .error "Flock lowering does not support interactions"
+
+/-- Successful affine lowering preserves evaluation for every assignment. -/
+theorem lowerAffine_correct (expression : Expression Bit) (affine : Affine)
+    (h : lowerAffine expression = .ok affine) (env : Environment Bit) :
+    affine.eval env.get = expression.eval env := by
+  induction expression generalizing affine with
+  | var v => simp [lowerAffine] at h; subst affine; rfl
+  | const c =>
+    simp only [lowerAffine] at h
+    split at h
+    · rename_i hc; cases h; simp [Affine.eval, Expression.eval, hc]
+    · split at h
+      · rename_i hc; cases h; simp [Affine.eval, Expression.eval, hc]
+      · cases h
+  | add a b ia ib =>
+    cases ha : lowerAffine a with
+    | error e => simp [lowerAffine, ha] at h
+    | ok aa =>
+      cases hb : lowerAffine b with
+      | error e => simp [lowerAffine, ha, hb] at h
+      | ok bb =>
+        simp [lowerAffine, ha, hb] at h
+        subst affine
+        simp [Affine.eval, Expression.eval, ia _ ha, ib _ hb]
+  | mul a b => simp [lowerAffine] at h
+
+private theorem bit_add_eq_zero_iff (a b : Bit) : a + b = 0 ↔ a = b := by
+  simpa only [sub_eq_add_neg, ZMod.neg_eq_self_mod_two] using
+    (sub_eq_zero : a - b = 0 ↔ a = b)
+
+/-- The exported rows characterize all satisfying source witnesses, not just honest evaluation. -/
+theorem lower_correct (operations : List (FlatOperation Bit)) (rows : List Row)
+    (h : lower operations = .ok rows) (env : Environment Bit) :
+    rows.Forall (Row.Holds env.get) ↔ FlatOperation.ConstraintsHoldFlat env operations := by
+  fun_induction lower operations generalizing rows <;>
+    simp_all [FlatOperation.ConstraintsHoldFlat, Expression.eval]
+  subst rows
+  rename_i ir output a b rest left ha right hb tail ht ih
+  have ea := lowerAffine_correct a left ha env
+  have eb := lowerAffine_correct b right hb env
+  simp only [List.forall_cons, Row.Holds, ea, eb, bit_add_eq_zero_iff, ih]
+
+theorem lower_no_interactions (operations : List (FlatOperation Bit)) (rows : List Row)
+    (h : lower operations = .ok rows) : FlatOperation.interactions operations = [] := by
+  fun_induction lower operations generalizing rows <;>
+    simp_all [FlatOperation.interactions]
+
+theorem lookup_rejected (lookup : Lookup Bit) (rest : List (FlatOperation Bit)) :
+    lower (.lookup lookup :: rest) = .error "Flock lowering does not support lookups" := rfl
+
+theorem interaction_rejected (interaction : AbstractInteraction Bit) (rest : List (FlatOperation Bit)) :
+    lower (.interact interaction :: rest) = .error "Flock lowering does not support interactions" := rfl
+
+end LeanVMCircuits.Flock
diff --git a/verification/circuits/README.md b/verification/circuits/README.md
new file mode 100644
index 000000000..535d35afd
--- /dev/null
+++ b/verification/circuits/README.md
@@ -0,0 +1,49 @@
+# Clean-authored production circuits
+
+The 64-bit wrapping adder in `crates/flock/src/clean.rs` is generated from the Clean circuit `LeanVMCircuits.WrappingAdder.adder64`. `Load::circuit`, `Store::circuit`, and `Ld::circuit` in `crates/leanvm_core/src/rv/semantics/memory.rs` call this generated function. `Sd` shares the `Ld` circuit. The Flock reduction regression also uses the same production function, not another handwritten adder.
+
+The same source also generates the 32-bit wrapping adder used by the production BLAKE2s circuit and the 64-bit carry-in/carry-out adder used by ALU, signed multiplication corrections, and division constraints. Division's conditional negation composes affine bit flipping with the exported carry adder. The former handwritten ripple-adder methods are removed. All optimized Rust word and packed witness kernels remain unchanged.
+
+These are Boolean circuits over `F2 = ZMod 2`, not Clean's prime-field `Addition32` gadget. Input and output vectors are little-endian bits; each element of `F2` is necessarily zero or one. Wrapping sums are modulo `2^64` or `2^32`, with 63 or 31 products in least-significant-bit order and no discarded-overflow product. The carry adder uses 64 ordered products and returns a 64-bit sum and one carry bit.
+
+## Reproduce
+
+The project pins Lean `v4.33.1`, Clean revision `b449bf590f93e13827c3c7e747e392d6969aa380`, and all transitive dependencies in `lake-manifest.json`. Regeneration uses Rust `1.97.0` with `rustfmt` and the repository's formatting configuration. Normal Rust builds use the checked-in generated file and require neither Lean nor a Clean checkout, network access, or a local filesystem dependency.
+
+From this directory:
+
+```sh
+lake exe cache get Mathlib.Tactic
+lake build
+lake env lean Audit.lean
+lake env leanchecker LeanVMCircuits
+lake env lean --run Generate.lean ../../crates/flock/src/clean.rs
+lake env lean --run Generate.lean /tmp/clean-generated.rs
+diff -u ../../crates/flock/src/clean.rs /tmp/clean-generated.rs
+```
+
+The `Clean circuits` workflow performs the proof build, axiom audit, serialized theorem kernel recheck, and deterministic regeneration check. The generator rejects unbound, forward, or duplicate product variables. The lowering accepts only affine GF(2) expressions and scalar witnesses immediately constrained to their defining products. Other witnesses, assertions, nested products in affine operands, lookups, interactions, and excessive subcircuit nesting return explicit errors rather than being ignored.
+
+## What is proved
+
+`FullAdder.soundness` proves the integer identity `sum + 2 * carry_out = x + y + carry_in` from the defining Boolean product constraint. Its completeness theorem checks the Clean witness generator. `Adder.circuit` composes those circuits with a proof of the full word identity. `WrappingAdder.circuit` removes the unused high carry product and proves the modular sum.
+
+`Flock.lowerAffine_correct` and `Flock.lower_correct` prove evaluation and constraint equivalence for every assignment. `Flock.flatten_correct` proves that successful bounded flattening returns exactly Clean's flat operations; the bound is an explicit export error, not a silently truncated circuit. `Flock.adder64_source` identifies the exact checked artifact with lowering of the actual Clean source. `Flock.adder64_layout` checks 63 ordered product variables starting at 128 and 64 outputs. `Flock.adder64_soundness` proves that every assignment satisfying that artifact's product constraints has the correct modular output. It does not assume that an assignment was generated honestly.
+
+`Flock.witness_exists` constructs satisfying assignments for acyclic product rows. `Flock.adder64_wellFormed` checks the concrete artifact's dependency order, and `Flock.adder64_complete` proves that every assignment of the 128 input bits extends to a satisfying assignment. Completeness therefore does not stop at an unfulfilled witness-generation premise.
+
+`Flock.adder32_source`, `adder32_layout`, `adder32_soundness`, `adder32_wellFormed`, and `adder32_complete` establish the corresponding exact-artifact claims for the 32-bit wrapping adder. Its product variables are 64 through 94, after 64 input bits. `Flock.carryAdder64_source`, `carryAdder64_layout`, `carryAdder64_soundness`, `carryAdder64_wellFormed`, and `carryAdder64_complete` establish them for the carry adder. Its input variables 0 through 127 name the operand bits, input 128 names the carry-in, and product variables 129 through 192 name 64 ordered products. The 65 output bits represent the exact integer `x + y + carry_in`, so the theorem covers both the low sum and final carry. Each completeness theorem extends every input assignment to a satisfying assignment.
+
+Artifact support, layout, and well-formedness are checked by `decide +kernel`, not `native_decide`. `Audit.lean` prints the transitive theorem axiom closures and fails on any axiom outside `propext`, `Classical.choice`, and `Quot.sound`. No admitted theorem, native-decision axiom, or security premise is used.
+
+## Rust interpretation and remaining trust
+
+The generator consumes the checked `Flock.adder64`, `Flock.adder32`, and `Flock.carryAdder64` artifacts directly. Input variables name the function's operand bits and, for the carry variant, its `carry_in` argument. Each later variable names the result of its ordered product. An affine zero or one becomes `Wire::ZERO` or `Wire::ONE`, affine addition becomes `Builder::xor`, and each row becomes `Builder::and`. Artifact outputs become the returned sum wires and, where present, carry wire. Generated common-subexpression reuse changes XOR gate ordering, not affine meaning or the order of products.
+
+`Builder` places ports before its constant pin and product slots. For the `Ld`/`Sd` shape, input bits occupy 0 through 127, output bits occupy 128 through 191, the constant pin is 192, and the 63 product slots occupy 193 through 255. The source's product variable 128 plus its ordinal maps to the corresponding Builder product, not to output slot 128 plus that ordinal. Builder output rows tie the committed output ports to the returned affine expressions. Structural zeros and unused port bits retain Builder's existing forced-zero interpretation.
+
+The proven export boundary is the concrete Lean artifact and its GF(2) semantics. Lean's runtime execution, the Rust pretty-printer and formatter, the Rust compiler, and Builder's implementation of XOR, AND, constant pinning, output rows, and slot packing remain trusted parts of the Rust interpretation. Deterministic regeneration checks linkage and drift; it is not presented as a proof of these implementations. The existing packed native `address_rows` witness kernel is unchanged. Its correspondence to the generated circuit is exercised by the production memory witness regression and complete RV proof verification, but the Rust native word-arithmetic implementation itself is not formally verified here.
+
+The RV regression `clean_adder_memory_addresses_wrap_and_carry` proves and verifies real `Ld`/`Sd` accesses through both a negative-immediate overflow and a long carry boundary, then rejects an altered output statement. The Flock reduction regression verifies honest batches and rejects mutations of input, output, constant, and product bits. This establishes exercised integration, not a cryptographic security proof of Flock, the PCS, Fiat-Shamir, or the whole VM. Other instruction circuits and protocol constraints are outside this adder proof.
+
+`clean_carry_adder_arithmetic_boundaries` proves and verifies actual ALU overflow and unsigned comparison, signed division overflow, and signed high multiplication, then rejects an altered output statement. The existing BLAKE2s precompile proof regression exercises the generated 32-bit adder. These are integration checks: the complete ALU, division, multiplication, BLAKE2s, and conditional-negation semantics are not yet formally proved by the adder theorems alone.
diff --git a/verification/circuits/lake-manifest.json b/verification/circuits/lake-manifest.json
new file mode 100644
index 000000000..34e3a3e0e
--- /dev/null
+++ b/verification/circuits/lake-manifest.json
@@ -0,0 +1,141 @@
+{
+ "version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages": [
+  {
+   "url": "https://github.com/kevaundray/clean.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "b449bf590f93e13827c3c7e747e392d6969aa380",
+   "name": "Clean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "b449bf590f93e13827c3c7e747e392d6969aa380",
+   "inherited": false,
+   "configFile": "lakefile.lean"
+  },
+  {
+   "url": "https://github.com/Verified-zkEVM/CompPoly.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "a09455a22fea4623a2a1c5b363cf6efc61486a83",
+   "name": "CompPoly",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.1",
+   "inherited": true,
+   "configFile": "lakefile.lean"
+  },
+  {
+   "url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "0df444a360eaa60ab8c11dca51a86af692955474",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.1",
+   "inherited": true,
+   "configFile": "lakefile.lean"
+  },
+  {
+   "url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"
+  },
+  {
+   "url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  }
+ ],
+ "name": "LeanVMCircuits",
+ "lakeDir": ".lake",
+ "fixedToolchain": false
+}
diff --git a/verification/circuits/lakefile.toml b/verification/circuits/lakefile.toml
new file mode 100644
index 000000000..8f852028b
--- /dev/null
+++ b/verification/circuits/lakefile.toml
@@ -0,0 +1,11 @@
+name = "LeanVMCircuits"
+version = "0.1.0"
+defaultTargets = ["LeanVMCircuits"]
+
+[[require]]
+name = "Clean"
+git = "https://github.com/kevaundray/clean.git"
+rev = "b449bf590f93e13827c3c7e747e392d6969aa380"
+
+[[lean_lib]]
+name = "LeanVMCircuits"
diff --git a/verification/circuits/lean-toolchain b/verification/circuits/lean-toolchain
new file mode 100644
index 000000000..a8afa7d1b
--- /dev/null
+++ b/verification/circuits/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.33.1