> ## Documentation Index
> Fetch the complete documentation index at: https://docs.theformalera.com/llms.txt
> Use this file to discover all available pages before exploring further.

# Deploy on AWS

> The CDK app that runs Spec Hub: storage, the API and website, and the solve workers.

`infra/` is an AWS CDK app (Python). It deploys three stacks per stage:

| Stack | Contents |
| - | - |
| `TheFormalEra-<Stage>-Data` | KMS key; an S3 object store (spec packages, results cache, requests and responses; versioned, KMS-encrypted); DynamoDB `Jobs` and `Tokens` tables; an SQS verification queue with a dead-letter queue |
| `TheFormalEra-<Stage>-Hub` | The Hub API (container Lambda + HTTP API, throttled); the website bucket; CloudFront (`/v1/*` → API, everything else → site); optionally an ACM certificate and a Route 53 alias `hub.<domain>` |
| `TheFormalEra-<Stage>-Solver` | A VPC (public subnets, no NAT gateway; tasks get a public IP and no inbound rules; S3 and DynamoDB gateway endpoints; flow logs); ECS Fargate workers (Spot first) draining the queue, scaled 0 → `workerMaxTasks` on queue depth; the Lemma Hub admission task every 3 days; DLQ and backlog alarms to SNS |

Images are built from the repository root: `infra/docker/hub-api.Dockerfile` (Lambda) and `infra/docker/worker.Dockerfile` (engine + Lean 4 + a prebuilt Mathlib cache).

## Deploy

```bash theme={"system"}
cd infra
uv sync --group dev
uv run --group dev pytest tests          # synthesis tests: no AWS account or Docker needed
npx cdk synth
npx cdk deploy --all \
  -c theformalera:stage=prod -c theformalera:domain=theformalera.com \
  -c theformalera:hostedZoneId=Z0123456789 -c theformalera:alarmEmail=oncall@example.com
```

## Context keys

| Key | Meaning |
| - | - |
| `theformalera:stage` | Stage name (`prod`, `staging`, …). Production retains the store, tables and key on deletion; other stages are destroyable. |
| `theformalera:domain` | Serve the Hub at `hub.<domain>` |
| `theformalera:hostedZoneId` | Route 53 zone of the domain: the stack creates, validates and aliases the certificate |
| `theformalera:certificateArn` | An existing ACM certificate in `us-east-1`, for DNS hosted elsewhere |
| `theformalera:alarmEmail` | Where DLQ and backlog alarms go |
| `theformalera:workerMaxTasks`, `workerCpu`, `workerMemoryMiB` | Solve-worker scaling and size |
| `account`, `region` | Target account and region (default `us-east-1`) |

### Custom domain with DNS outside Route 53

CloudFront only accepts ACM certificates from `us-east-1`.

1. Request a certificate for `hub.<domain>` in `us-east-1`: `aws acm request-certificate --region us-east-1 --validation-method DNS …`.
2. Add its validation CNAME at your DNS provider (DNS only, not proxied; keep it for renewals).
3. When it is `ISSUED`, set `theformalera:certificateArn` and deploy.
4. Point a CNAME `hub` at the `CdnDomain` stack output.

### Fargate quotas

The default worker size (3 × 4 vCPU / 16 GiB) fits a new account's Fargate quotas of 12 Spot and 12 On-Demand vCPUs; the admission task takes 4 On-Demand vCPUs. Larger workers (for example 16 vCPU / 64 GiB × 32) need the `Fargate Spot vCPU resource count` (L-36FBB829) and `Fargate On-Demand vCPU resource count` (L-3032A538) quotas raised first. A task larger than the quota is never placed.

## After the first deploy

```bash theme={"system"}
# publish the specs (builds the Lean library, audits the proofs, signs every package)
uv run theformalera-hub keygen -o publisher.pem            # once; keep the key in a secret store
uv run theformalera-hub publish --specs specs --store s3://<StoreBucket> --version 1.0.0 --key publisher.pem
```

You never upload the website by hand. A site Lambda renders it from the store, uploads the files that changed and invalidates CloudFront:

* during `cdk deploy`, whenever the Hub image changed (a failed render fails the deploy);
* after each publish, advisory or Lemma Hub admission (the store bucket sends its writes to EventBridge).

To re-render by hand, run `aws lambda invoke --function-name <SiteRendererName> /dev/stdout`.

Issue API tokens by putting items into the `Tokens` table: `{token_hash: sha256(token), tenant, plan, quota}`.


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.