Running Remotely with Modal¶

OpenATP supports running agentic provers remotely in Modal Sandboxes. Modal bills for compute per second – see current pricing. In this guide, we will authenticate with the Modal CLI, build the OpenATP Modal image, and test everything by verifying a small theorem.

Build the Modal image¶

Modal Sandbox containers are created from the same OpenATP default Docker image. Before running any prover, you must create the image on Modal. Build it with the open-atp CLI:

open-atp build-modal-image

Use the Modal CLI to check the image was created successfully.

$ modal image names list
┏━━━━━━━━━━━━━━━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━┓
┃ Tag                ┃ Image ID                  ┃ Updated at           ┃
┡━━━━━━━━━━━━━━━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━┩
│ open-atp:latest    │ im-9rcKV2cJKID4nhE4GQGbPm │ 2026-06-25 17:39 EDT │
└────────────────────┴───────────────────────────┴──────────────────────┘

The Docker image for Modal is nearly identical to the Dockerfile used to build the local Docker image. It is built programmatically using the modal Python package for more effective caching.

_build_modal_image()

def _build_modal_image(args: argparse.Namespace) -> int:
    """Build and publish the sandbox image on Modal via Modal's builder methods.

    Built programmatically (rather than from images/Dockerfile) so the Modal image
    can install the Lean toolchain + tools *globally as root*: Modal ignores a
    container ``USER`` and runs everything as root, so the agent-user layout the
    Docker image uses doesn't apply. Installing globally keeps `lake`/`lean`/`uv` on
    root's PATH and -- crucially -- leaves the baked Mathlib package git repos
    root-owned, so `lake` reads them cleanly instead of re-cloning (which would wipe
    the warm cache). Kept in sync with images/Dockerfile; the two notable differences
    are exactly "global/root install" and "no ENTRYPOINT/agent user".

    Publishes a named image the ``ModalBackend`` looks up with
    ``modal.Image.from_name(name)``.
    """
    try:
        import modal
    except ModuleNotFoundError:
        print(
            "the modal compute backend requires the `modal` package; "
            "install it with `pip install open-atp`.",
            file=sys.stderr,
        )
        return 1

    lean_dir = Path(__file__).resolve().parents[2] / "images" / "lean"
    if not (lean_dir / "lakefile.toml").is_file():
        print(f"No Lean skeleton at {lean_dir}", file=sys.stderr)
        return 1

    app = modal.App.lookup(name=args.app, create_if_missing=True)
    image = (
        modal.Image.from_registry("ubuntu:24.04")
        .env({"DEBIAN_FRONTEND": "noninteractive"})
        # ripgrep is recommended for lean-lsp-mcp's local search. force_build on the
        # base layer so --force cascades through every subsequent (cached) layer.
        .run_commands(
            "apt-get update && apt-get install -y --no-install-recommends "
            "ca-certificates curl git unzip build-essential python3 python3-pip "
            "pipx ripgrep procps && rm -rf /var/lib/apt/lists/*",
            force_build=args.force,
        )
        # Node 20 + agent CLIs (Claude Code, Codex, OpenCode, Kimi Code), installed
        # globally. @moonshot-ai/kimi-code provides the `kimi` CLI the KimiHarness uses.
        .run_commands(
            "curl -fsSL https://deb.nodesource.com/setup_20.x | bash - "
            "&& apt-get install -y --no-install-recommends nodejs "
            "&& npm install -g @anthropic-ai/claude-code @openai/codex opencode-ai "
            "@moonshot-ai/kimi-code "
            "&& rm -rf /var/lib/apt/lists/*"
        )
        # elan + Lean toolchain in a global ELAN_HOME so `lake`/`lean` are on root's
        # PATH. --default-toolchain none lets images/lean/lean-toolchain pin it.
        .env({"ELAN_HOME": "/opt/elan"})
        .run_commands(
            "curl https://raw.githubusercontent.com/leanprover/elan/master/"
            "elan-init.sh -sSf | sh -s -- -y --default-toolchain none "
            "--no-modify-path"
        )
        # pipx tools (lean-lsp-mcp, uv, mistral-vibe) to global dirs so their
        # entrypoints land on PATH. mistral-vibe provides the `vibe` CLI the
        # VibeHarness drives; pinned so the builtin `lean` agent's model pin (Leanstral
        # 1.5) stays stable across rebuilds (keep in sync with images/Dockerfile).
        # Shared uv cache for the Numina skills' `uv run` deps.
        .env({"PIPX_HOME": "/opt/pipx", "PIPX_BIN_DIR": "/usr/local/bin"})
        .env({"UV_CACHE_DIR": "/opt/uv-cache"})
        .run_commands(
            "pipx install lean-lsp-mcp && pipx install uv "
            "&& pipx install mistral-vibe==2.19.0"
        )
        # ax-prover (LangGraph Lean agent) backing the AxProverBaseHarness,
        # pipx-isolated from open-atp and the CLIs. Keep AX_PROVER_REF in sync with the
        # images/Dockerfile ARG. Pinned to a git commit (not a PyPI release) for the
        # lean_interact target discovery -- see AX_PROVER_SPEC above.
        .run_commands(f"pipx install '{AX_PROVER_SPEC}'")
        # Modal's .env() sets literal values (no ${PATH} expansion like Dockerfile
        # ENV), so set an explicit PATH with /opt/elan/bin ahead of the standard dirs.
        .env(
            {
                "PATH": "/opt/elan/bin:/usr/local/sbin:/usr/local/bin:"
                "/usr/sbin:/usr/bin:/sbin:/bin"
            }
        )
        .workdir("/workspace")
        # copy=True bakes the skeleton into a build layer so the lake steps can read
        # it. lake update resolves the manifest + clones mathlib (installing the
        # pinned toolchain); cache get downloads its oleans for a warm cache.
        .add_local_dir(str(lean_dir), "/workspace", copy=True)
        .run_commands("lake update && lake exe cache get")
        # Pre-warm the uv cache with the Numina skills' PEP 723 deps (matches the
        # Docker image), so the first `uv run` in the sandbox resolves from cache.
        .run_commands(
            "printf '%s\\n' "
            "'# /// script' '# requires-python = \">=3.11\"' "
            '\'# dependencies = ["requests", "google-genai", "openai", '
            "\"anthropic\"]' '# ///' 'print(\"warmed\")' > /tmp/warm_skills.py "
            "&& uv run --no-project /tmp/warm_skills.py && rm /tmp/warm_skills.py"
        )
        # No ENTRYPOINT: the ModalBackend execs the wrapped command directly after
        # pushing the workdir.
    )
    with modal.enable_output():
        built = image.build(app)
    built.publish(args.name)

    print(f"Published Modal image {args.name!r} (app {args.app!r}).")
    print("Reference it from a Sandbox with:")
    print(f"    modal.Image.from_name({args.name!r})")
    return 0

Test the image¶

To confirm the image was built correctly, use the test method below. It verifies a trivial proof inside the Modal Sandbox container. No prover is run and no agent credentials are needed.

from open_atp.backends.modal import ModalBackend

assert ModalBackend().test()

Configure and monitor resources¶

ModalBackend accepts cpu (a guaranteed floor of cores; the Sandbox may burst higher) and memory_mib (in MiB). It is recommended to budget at least 2 CPUs and 4 GB of memory. This was found to achieve a good time/cost tradeoff.

from open_atp.backends.modal import ModalBackend

backend = ModalBackend(cpu=2.0, memory_mib=4096)

Live Sandboxes, their resource usage, and per-second cost are visible from the Modal dashboard. You can also terminate runaway jobs from the dashboard.

Running Remotely with Modal¶

Authenticate with the Modal CLI¶

Build the Modal image¶

Test the image¶

Configure and monitor resources¶