Build and run ACIR formal proof tests with SMT verification. Generates ACIR artifacts from noir's ssa_verification tool, then runs each test individually with user-specified time/memory limits, and updates the README results table.
Run the full ACIR formal verification pipeline: build tests, generate artifacts, and run each test with resource limits.
SMT=ON and ACIR_FORMAL_PROOFS=ON flagsConfigure cmake with SMT support and build:
cd barretenberg/cpp
cmake --preset smt-verification -DACIR_FORMAL_PROOFS=ON
cd build-smt && ninja acir_formal_proofs_tests
The preset smt-verification already sets SMT=ON. We additionally need ACIR_FORMAL_PROOFS=ON.
If the build has already been configured, just run ninja acir_formal_proofs_tests from .
build-smt/Check if the submodule is populated:
ls noir/noir-repo/tooling/ssa_verification/Cargo.toml 2>/dev/null
If the file doesn't exist, initialize the submodule:
git submodule update --init --depth 1 noir/noir-repo
ALWAYS run this step — even if .acir files already exist in /tmp/. The artifacts must be regenerated every time to ensure they match the current noir compiler version.
cd noir/noir-repo
cargo run --release -p ssa_verification -- --dir /tmp/
This generates .acir files in /tmp/ that the C++ tests load. The tool compiles Noir SSA instructions into ACIR format for each operation (add, sub, mul, div, etc.) with various type combinations.
Before running tests, ask the user:
What is the maximum time (in seconds) and memory (in GB) you'd like to allow per test? Some tests are very fast (<10s) while others can take hours or days. Known heavy tests:
Test Typical time Typical memory uint_terms_shl32 ~4574s ~30GB uint_terms_shl8 ~4574s ~30GB uint_terms_shr ~3928s ~10GB uint_terms_xor ~355s - uint_terms_div days 20GB uint_terms_mod >130 days 3.2GB integer_terms_div >17 days 20GB non_uniqueness_for_truncate_field_to_u64 hours - Suggested defaults: 600 seconds, 16 GB (skips the heaviest tests)
Wait for the user to provide limits before proceeding.
Use the run_tests.sh script bundled with this skill. It runs all tests sequentially with the user's time/memory limits and writes results to /tmp/acir_test_results.txt.
.claude/skills/acir-formal-proofs/scripts/run_tests.sh ${TIME_LIMIT} ${MEM_LIMIT_GB}
For example, with 600s timeout and 16GB memory limit:
.claude/skills/acir-formal-proofs/scripts/run_tests.sh 600 16
The script handles timeout/OOM detection, wall-clock timing via /usr/bin/time -v, and prints a summary table at the end. Results are saved to /tmp/acir_test_results.txt in pipe-delimited format.
CRITICAL: Do NOT run tests any other way. Do NOT launch multiple tests in parallel — these tests are extremely memory- and CPU-intensive (some use >30GB RAM).
After all tests complete, update the results table in:
barretenberg/cpp/src/barretenberg/acir_formal_proofs/README.md
For each test that was run, update the corresponding row:
✓ if passed, ✗ if failed/timeout/OOM- if passed, otherwise "Test takes too long", "OOM", or the failure reasonThe mapping from test name to README row is by opcode + types. For example:
uint_terms_add -> Binary::Add | Unsigned_128 | Unsigned_128field_terms_add -> Binary::Add | Field | FieldSignedAdd -> Binary::Add | Signed_64 | Signed_64uint_terms_not -> Not | Unsigned_128 | -non_uniqueness_for_truncate_u64_to_u8 -> Truncate | Unsigned_64 | Unsigned_8Do NOT modify rows for tests that were not run (e.g., if they timed out in a previous run and were skipped).
Add new rows if any tests exist in the test file but not in the README table.