Infrastructure as code, in Lean 4

Terraform-style declarative infrastructure, written in the Lean programming language and proof assistant instead of a bespoke DSL. Target and observed cloud state are dependently-typed Lean values, so an unrealisable target is a compile error rather than a failed apply.

A dangling reference, a region a cloud is not in, an instance size that does not exist, a plaintext password in a committed file — none of these get as far as a plan.

3clouds — AWS, Scaleway, GCP

14resource kinds

Read the tutorial View on GitHub

Declare a fleet

A complete, working declaration. The resource's name is written once and is the cloud's real identifier.

Main.lean

-- One bucket in Paris. `in paris` is what places it:
-- AWS would read eu-west-3, Scaleway fr-par.
fleet myFleet in paris where
  provider scaleway where
    resource objectStore "my-first-bucket"
      { versioning := true
      , tags       := [("project", "tutorial")] }

def main (args : List String) : IO UInt32 :=
  Infra.Cli.run "my-infra" myFleet.plan
    (regions := myFleet.regions) (args := args)

-- Blocks nest and scope like a `with` in Python.
fleet spread in paris where
  provider aws where
    resource s3Bucket "eu-assets" { versioning := true }

    in nVirginia where
      resource s3Bucket "us-east-assets" { versioning := true }

  provider scaleway where
    in amsterdam where
      resource objectStore "nl-cache" { versioning := true }

-- Scaleway has no Oregon region, so this does not compile:
--   Assert (Locality.oregon.code ProviderId.scaleway).isSome
--   is false

fleet web in paris where
  provider aws where
    resource securityGroup "web" as webGroup
      { description := "http from anywhere" }

    resource awsInstance "web-1"
      { imageId       := "ami-0d3c032f5934e1b41"
      , instanceType  := InstanceType.of .t3 .nano
      , securityGroup := webGroup }

-- The reference is an index into this fleet's own keys, so it
-- cannot dangle, cannot name the wrong kind, cannot name the
-- wrong cloud. The group is created first because of it.

resource secrets "db-password" as dbPassword
  { valueFrom := fromEnv "DB_PASSWORD" }

resource postgres "main" as mainDb
  { masterUsername       := "dbadmin"
  , masterPasswordSecret := "db-password"
  , minCapacity := 1, maxCapacity := 4 }

-- A value that cannot exist until the database does.
-- Both references become ordering edges, so ONE apply
-- creates all three, in the right order.
resource secrets "db-url"
  { valueFrom := composed
      expr!"postgres://dbadmin:{secretValueOf dbPassword}
              @{endpointOf mainDb}/main" }

Clouds

What the compiler catches

Not a validation pass that runs before apply. These are type errors and decidable side-conditions, settled while the file elaborates — so the failure arrives in your editor, not after half a fleet exists.

References cannot dangle

A reference has the type of an index into this fleet's own keys. There is no "not found" case to handle, a bucket key is a different type from a security-group key, and keys are indexed by cloud as well as kind. Ordering falls out of the same fact: the scheduler reads the reference graph, handles arbitrary DAGs, and rejects cycles by name.

the error

-- pointing at a bucket where a security group belongs
Application type mismatch: The argument
  bucket
has type
  keys.Key ProviderId.aws Kind.s3Bucket
but is expected to have type
  Expr keys.Key (keys.Key ProviderId.aws Kind.securityGroup)

A cloud cannot be somewhere it is not

A locality is a place named before any cloud names it, so one in paris resolves to eu-west-3 on AWS and fr-par on Scaleway. Scaleway has a Warsaw region and AWS does not — so in warsaw compiles for a Scaleway-only fleet and fails for one that also uses AWS.

the error

fleet crossCloud in warsaw where …

Tactic `decide` proved that the proposition
  Assert (Locality.warsaw.covers keys)
is false

Instance types are a family and a size

Not a string. Twenty-six current families share nine size lists between them, so the pair is checked: t3 stops at 2xlarge, and gen-7 Intel skips 32xlarge entirely and jumps to 48xlarge. Autocomplete lists the families, then the sizes it actually comes in.

the error

instanceType := InstanceType.of .t3 .xlarge32

Tactic `decide` proved that the proposition
  Assert (InstanceFamily.t3.sizes.contains InstanceSize.xlarge32)
is false

Secrets never hold a value

A secret names an environment variable, or a function over state that does not exist yet. The value is never known to the file, the plan output, or the on-disk cache. That a committed fleet holds no plaintext is itself decidable — #guard plan.secretsAreSound — so it is checked at compile time rather than trusted.

one apply, correctly ordered

would CREATE scaleway/secrets/db-password
would CREATE scaleway/postgres/main
would CREATE scaleway/secrets/db-url

-- the composed secret comes last because both its
-- references are ordering edges, not because anything
-- here lists an order

Why this instead of Terraform or OpenTofu

Not for the breadth — they have thousands of providers and this has three. For what the type system buys, which is a different thing and worth being precise about.

Errors move to compile time

A dangling reference, a reference of the wrong kind or the wrong cloud, a missing required field, a region a cloud is not in, an instance size that does not exist, a plaintext secret in the committed file. In HCL each of these is a plan-time or apply-time failure; here they are type errors and decidable side-conditions, so they fail in your editor. See the examples above — each is a real message.

Ordering is derived, not declared

There is no depends_on. A reference is the dependency, so the graph cannot disagree with the code — and both directions are sorted, so teardown is the reverse of the same graph rather than a guess. Cycles are rejected by name.

One apply, not two

A value that needs state which does not exist yet — a connection string wanting both a generated password and an endpoint the cloud assigns at creation — is written as a function over that state. Both references become ordering edges, so one apply does it. No second run, no operator pasting a string in between.

Secrets cannot be in the file

A secret names an environment variable or a composition — never a value. That a committed fleet holds no plaintext is itself decidable and checked at compile time, and no value reaches plan output or the on-disk cache.

One spec, either cloud

Portable kinds are indexed by kind alone, never by provider, so the same value applies to any cloud; the provider enters only at apply. Reaching for a cloud-specific concept makes the loss of portability visible in the type, not in a comment.

It is Lean, not a DSL

Loops, functions, abstraction and testing are the host language's, already there and already documented. Your fleet is a value you can compute with, and #guard lets you assert things about it that hold at build time. Apache-2.0, no CLA, no relicensing risk.

It converts both ways

toHcl turns a fleet into .tf — resource blocks, provider blocks from the placement, and real HCL references where the fleet has references, because a reference is an index into the fleet and so the target's type and label are both derivable. fleetOfState reads terraform show -json the other way and writes a fleet declaration.

Neither is claimed to be a round trip. What HCL cannot express — a composed secret, a value over post-apply state — comes out as a # TODO naming what was dropped, because a silently wrong value is worse than a visible hole.

generated main.tf

# A STARTING POINT, NOT A ROUND TRIP.

provider "aws" {
  region = "eu-west-3"
}

resource "aws_security_group" "web" {
  name        = "web"
  description = "http"
}

resource "aws_instance" "web-1" {
  ami                    = "ami-1"
  instance_type          = "t3.nano"
  vpc_security_group_ids = [aws_security_group.web.id]
}

How far this has actually been run

The part most project pages leave out — and the reason to trust the rest of this one. Every claim below was read out of a CI run or counted in the source, not estimated. Coverage is the full breakdown, kept current, and it names what has not been exercised as precisely as what has.

Verified live

Full create → converge → destroy round trips in CI on all three clouds — 12 resources on AWS, 12 on Scaleway, 10 on Google Cloud, across thirteen of the fourteen kinds. Each leg applies three declarations in sequence: the whole fleet, a version with two resources dropped and a field changed, then one that declares nothing. After every stage the account must hold exactly what that stage declares, so a resource whose line is gone has to be destroyed rather than abandoned. All three dependency shapes are covered: a chain, a fan-out, and a fan-in.

Proved on every build

SigV4 against AWS's published test vectors. DAG scheduling, checked against an independent topological-order checker on a sixteen-node graph. The credential chain and its redaction. Divergence and the mutability table. That no plaintext secret is in a committed file — decidable, so the compiler establishes it rather than a reviewer.

Not yet exercised

Four clients — Lambda, RDS, Cloud SQL, Scaleway's Managed Database and Functions — the kinds a test cannot arrange from nothing. Most update paths too: the sequence changes a queue's visibility timeout, so that one path runs on two clouds, and no other kind's does. Named here because a coverage claim you cannot check is worth nothing.

What the live tests actually do

Ten to twelve resources per cloud, and every step below is a real API call against a real account. Not a coverage matrix — a proof that the whole engine works end to end against three different APIs: the credential chain, region resolution, list, create, the diff, delete, settling, and the on-disk cache. Everything is named ci-tests-infra-…, and teardown runs even when the assertions fail.

Stage	What it declares	What it proves
1	the whole fleet	`create` works, the credential chain reached the right account, and the dependency order holds — a fan-out of two, a fan-in of three with a redundant edge, and a four-deep chain, all in one apply
2	two resources dropped, one field changed, one added	a resource whose line is gone gets destroyed rather than abandoned — only the ledger can name it. Plus `update` for the changed field and `create` for the new one
3	nothing at all	`delete` for everything left. This is `apply` against an empty declaration, which is the same operation `destroy` performs

After each stage the account must hold exactly what that stage declares, and each stage polls for that rather than reading once: every list API here is eventually consistent, so a single read after a write measures propagation delay rather than correctness.

Stage 2 is the one that earns the sequence. If a resource were considered managed because the declaration named it, its two dropped resources would be quietly abandoned, stage 3 would find nothing to clean up, and both stages would pass while leaking two billable resources per cloud. That is exactly what the first two rounds of these runs caught.

The fleets also have shape, not just size — a chain, a fan-out and a fan-in of dependencies — because ordering is the part of this engine most likely to be wrong in a way only a real cloud reveals, and each shape fails differently when the schedule is wrong. Two of the three were found to be broken this way: a container whose namespace reference made every plan propose a replace, so the fleet never converged.

Seven portable kinds — one spec value, any cloud, and every cell now has a live client behind it.
Kind	AWS	Scaleway	Google Cloud
`objectStore`	S3	Object Storage	Cloud Storage
`queues`	SQS	Queues	Pub/Sub
`secrets`	Secrets Manager	Secret Manager	Secret Manager
`imageRegistry`	ECR	Container Registry	Artifact Registry
`compute`	Lambda (image)	Serverless Containers	Cloud Run
`iam`	IAM users	IAM applications	Service accounts
`postgres`	RDS	Managed Database Serverless SQL when no instance class is set	Cloud SQL

And seven provider-local kinds. A dash is not a gap here — it is the point: these name a concept one cloud has and the others do not, so reaching for one makes the loss of portability visible in the type rather than in a comment. Declaring one on the wrong cloud is reported as having no counterpart, not as a missing client.

Kind	AWS	Scaleway	Google Cloud
`s3Bucket`	S3, with Object Lock	—	—
`securityGroup`	EC2 security groups	—	—
`awsInstance`	EC2 instances	—	—
`scalewayFunctionNamespace`	—	Functions namespaces	—
`scalewayFunction`	—	Serverless Functions	—
`scalewayContainerNamespace`	—	Containers namespaces	—
`scalewayContainer`	—	Serverless Containers	—

Fourteen kinds, three clouds. Every cell that is not a dash has a live client behind it — with two limits worth stating rather than discovering: a serverless postgres raises on Google Cloud, because Cloud SQL has no capacity range that scales to a floor, and iam there reads the roles bound to a service account but refuses to write them, since granting a role on GCP rewrites the whole project's policy.

Start a project

infra new scaffolds a declaration repository you can commit and deploy the same day: the canonical structure, a commented example fleet that compiles, and CI for GitHub and GitLab with the plan/apply split already wired. It builds on lake init, so Lake still owns the toolchain pin — what it adds is the part Lake cannot know about, chiefly the native link flags every consumer needs and would otherwise copy by hand — and it converts lakefile.toml to Lean, because those flags cannot be expressed in TOML. It writes only what is absent, so it is safe to re-run and safe on a project with work in it. Your declaration is a Lean program, so lake exe my_infra is the CLI: nothing to keep in step with your code. What it manages is a local ledger of names; what it last saw is a disposable cache. Neither is committed, and neither holds a secret.

shell

lake init my_infra && cd my_infra

# add to lakefile.toml:
#   [[require]]
#   name = "infra"
#   git = "https://github.com/typednotes/infra"
#   rev = "main"

lake update                # fetch infra
lake exe infra init        # turn this into an infra project
lake build
lake exe my_infra          # offline plan — free, no credentials
lake exe my_infra apply    # make it so

You get Fleet.lean (the whole declaration), Main.lean (five lines), a .gitignore that excludes the state cache, Catalogue.lean with every resource kind declared once to copy from, and pipelines for GitHub Actions, GitLab CI, CircleCI, Azure Pipelines and Jenkins — each planning on every push and applying only when a person presses the button. Fill in the account ids, add your secrets, commit.

Or read this one

A bare invocation is offline, credential-free and free of charge: it plans against placeholder backends. You have to ask for the real thing.

shell

git clone https://github.com/typednotes/infra && cd infra
lake build
lake exe infra              # offline self-checks
lake exe cross-cloud        # a plan spanning two clouds
lake exe multi-region       # six resources in four regions