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

17resource 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 (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 a dump snapshot. 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 a dump snapshot.

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

Every kind plans offline against a placeholder backend, and most have been created and destroyed against a real account. Which kinds, on which clouds, and how far — that is the coverage report, kept in the repo next to the tests it describes. Managed-cluster provisioning and deletion report elapsed time and the cloud's status while they wait; the opt-in Kubernetes live test budgets time for teardown as well as creation, and checks AWS role reads before provisioning. EKS's default-VPC selector is recognised on observation as well as creation.

Read the coverage report

Since 0.22.0, container tags such as :latest resolve to verified manifest digests before the live diff. Apply deploys that frozen content; an unchanged digest converges. See the image resolution guide for registry authentication and the Kubernetes scope.

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 decided by a marker on each resource, not a committed file — a tag where the cloud has tags, a marker written into the object’s description where it has not, and the resource’s own name against the fleet’s prefix for the two products with neither. The marker carries the fleet’s name — fleet myFleet is my-fleet — so two fleets sharing an account read each other’s resources as foreign and leave them alone. The markers are read from the cloud on every run and nothing is stored locally, so a fresh CI runner sees what your laptop sees. forget takes the marker off a tagged resource without deleting it, and dump writes that view as JSON, never a secret.

shell

lake init my_infra && cd my_infra

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

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 (the account ids, and one call handing the whole declaration to Infra.Cli.run), a .gitignore for Lake’s build output, 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