[shellygr]

Summary

This PR lets composer send its Claude requests to Amazon Bedrock instead of the Anthropic API. It covers composer only. certora_autosetup keeps calling the Anthropic API. The setting AUTOPROVER_LLM_BACKEND=bedrock turns it on. The default is anthropic, which builds the same chat model as master, so the merge changes nothing until someone sets the variable.

Composer reaches Bedrock through its "Mantle" endpoint, which accepts the Anthropic Messages API. The branch does not add langchain-aws, because that package needs langchain-core>=1.7.6 and this repo keeps langchain_core<1.3.3. A small subclass of ChatAnthropic uses the Anthropic SDK's own Bedrock Mantle clients instead.

Commits

1. Bump anthropic to a release with the Bedrock Mantle client (a77dc02). The anthropic pin becomes >=0.122.0,<1.0 with the bedrock extra. 0.122.0 is the first release whose async client signs requests and refreshes AWS credentials outside the event loop. The lock moves anthropic from 0.88.0 to 0.125.0 and changes no other package.

2. Add a Bedrock backend for Claude behind AUTOPROVER_LLM_BACKEND (39dbd7a). With bedrock, the chat model sends requests to the Mantle endpoint. The region comes from AWS_REGION or AWS_DEFAULT_REGION, and the default AWS credential chain signs the requests. Model ids stay logical (claude-opus-5-5) outside the client. Requests carry anthropic.<id>, and responses report the logical id, so usage, pricing and by_model do not change. Bedrock mode does not use the Files API uploader or its beta header.

3. Send PDFs inline on Bedrock within a request-size budget (3f6a84f). Bedrock has no Files API, so PDFs go inline as base64 document blocks that keep cache_control, also inside tool results. AUTOPROVER_BEDROCK_MAX_DOCUMENT_BYTES (8,000,000) and AUTOPROVER_BEDROCK_MAX_REQUEST_BYTES (16,000,000) keep each request under the 20 MB Bedrock limit. A document that does not fit becomes a short text note with its name, so a run never fails on size. A thread checkpointed with Files API references stops with a clear message before its first Bedrock request.

4. Cap max_tokens on Bedrock and retry its transient errors (9432d72). Bedrock counts max_tokens against the input-token quota before the model answers. So Bedrock requests use AUTOPROVER_BEDROCK_MAX_TOKENS (64,000 by default), and the Anthropic path keeps 128,000. The code retries throttling, model-not-ready, 5xx, timeouts, transient stream errors and short credential-fetch failures. It does not retry access denied, unknown model or validation errors.

5. Document Claude on Bedrock and guard AWS credentials in the sandbox (b618f1a). The README has a Bedrock section: the switch, the region, credentials, the IAM permission, the token cap, the PDF limits and the logical model ids. The Docker wrapper and compose file pass the Bedrock settings through. The sandbox escape test makes sure that confined code cannot see AWS_* variables or reach the container credential endpoint or the IPv6 metadata endpoint.

6. Fix Bedrock credential, retry and log handling (bfb5191). This commit holds the fixes from a review of the whole branch. With no AWS credentials, a request fails with BedrockCredentialsError, and the run does not retry it. The chat model replaces every model name in a response, including versioned and ARN forms, with its own id. If an error body has no type, the retry check reads the x-amzn-errortype header. Each dropped document gets one WARNING. The Docker wrapper accepts a Bedrock API key in place of static AWS keys.

7. Name the copied types in the payload-walk docstring (920532b). A wording change in one docstring. No code changes.

Testing

• python -m pytest tests -q -m "not expensive": 2238 passed, 10 skipped.
• pyright composer/: 0 errors.
• No Bedrock account was used. All Bedrock tests use mocked clients and transports.

Not tested against a live account

• The Mantle wire format: base64 PDF blocks inside tool_result, the shape of error bodies, and the model name in a response. The code does not depend on that name.
• The 64,000 max_tokens default comes from reading the call sites, not from a measurement.
• The IAM statement in the README comes from the AWS docs.

Notes for review

• The SDK bump (0.88.0 to 0.125.0) also affects the default Anthropic path and certora_autosetup. The tests pass. Master reaches prod automatically, so one dev run on the default backend before the merge is worth it.
• In Bedrock mode, each checkpoint stores the inline PDF bytes, not a file id. OpenRouter already works this way. A large design PDF in a long run makes the checkpoint database grow.

🤖 Generated with Claude Code