Deploy on AWS - The Formal Era

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

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.

Request a certificate for hub.<domain> in us-east-1: aws acm request-certificate --region us-east-1 --validation-method DNS ….
Add its validation CNAME at your DNS provider (DNS only, not proxied; keep it for renewals).
When it is ISSUED, set theformalera:certificateArn and deploy.
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

# 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}.

​Deploy

​Context keys

​Custom domain with DNS outside Route 53

​Fargate quotas

​After the first deploy

Deploy

Context keys

Custom domain with DNS outside Route 53

Fargate quotas

After the first deploy