Summary

uv pip install -e . (and equivalently pip install -e .) fails on macOS arm64 with Apple Clang 15 because z3-solver==4.16.0.0 has no prebuilt wheel for this platform, forcing a source build of Z3 itself — which then fails on Apple Clang 15's incomplete C++20 <format> support.

Environment

• macOS arm64 (Apple Silicon)
• Python 3.12.8 (via uv)
• Apple Clang 15.0.0 (Xcode default on this machine)
• Existing system Z3 4.15.4 (installed separately via Homebrew, not used by Vera)
• Vera repo: HEAD of main as of 2026-05-21

What I tried

Followed the official install steps from veralang.dev/SKILL.md:

git clone https://github.com/aallan/vera.git && cd vera
python -m venv .venv && source .venv/bin/activate  # also tried `uv venv`
pip install -e .

What happened

pip resolves z3-solver==4.16.0.0, which has only an sdist on PyPI for arm64 macOS (the latest published wheel for macosx_*_arm64 is z3_solver-4.9.1.0-py2.py3-none-macosx_11_0_arm64.whl). The sdist is built via CMake. The build fails compiling src/ast/array_decl_plugin.cpp and src/ast/ast.cpp with errors like:

error: no member named 'format' in namespace 'std'
        m_manager->raise_exception(std::format("map expects to take as many arguments ...", ...));
                                   ~~~~~^

The std::format header was added in C++20 (P0645) but Apple Clang 15 doesn't have the libc++ implementation yet — it landed in Clang 17 / libc++ 17. So Z3 4.16.0's source build is effectively broken on the default Apple toolchain on macOS arm64.

Full build log available on request.

Why this matters for adoption

vera/SKILL.md explicitly tells AI agents in sandboxed environments to expect the install to work:

For agents running in a sandbox (Claude.ai, Code Interpreter, container-based execution environments, etc.): the steps above work. Sandboxes typically have Python, git, pip, and outbound network access — that's all Vera needs.

But on the most common modern macOS development environment (Apple Silicon + default Xcode Clang), the install hits this wall before producing a working vera binary. Any AI agent following the documented steps will conclude Vera "isn't available" and move on.

Suggested fixes (any of these would help)

1. Pin z3-solver to a version with prebuilt arm64-macos wheels (e.g. z3-solver>=4.12,<4.15 — let me know if Vera needs specific 4.16 API surfaces).
2. Loosen the pin to a range that allows pip to pick a prebuilt wheel where available.
3. Document the Apple Clang 15 issue in SKILL.md with the workaround (install Xcode 16 / Clang 17, OR use a Linux container).
4. Allow linking against system Z3 via an env var (e.g. VERA_USE_SYSTEM_Z3=1) — many users already have a working z3 from Homebrew.

Context

I ran into this while building AILANG's eval harness — wiring Vera as a peer language for a comparative benchmark suite inspired by the Negroni Venture Studios "Three Camps Alike in Dignity" post that surveys 16 AI-native languages including Vera. Happy to share the AILANG harness pattern if useful — single-file evaluation (vera run <file>.vera) would slot in cleanly the same way MoonBit did, once the install stops failing.

Filing this here so other AI agents (and humans) hitting the same wall can find the diagnosis and your eventual fix.