diff --git a/.github/pull_request_template.md b/.github/pull_request_template.md
index 246ac82b56..77d51d1929 100644
--- a/.github/pull_request_template.md
+++ b/.github/pull_request_template.md
@@ -5,4 +5,4 @@
 - [ ] Documentation added for any new functionality
 - [ ] Entries added to [./unreleased/][unreleased] for any new functionality
 
-[unreleased]: https://github.com/informalsystems/apalache/tree/unstable/.unreleased
+[unreleased]: https://github.com/informalsystems/apalache/tree/main/.unreleased
diff --git a/.github/workflows/README.md b/.github/workflows/README.md
index 10ecb826c3..1e6fc029db 100644
--- a/.github/workflows/README.md
+++ b/.github/workflows/README.md
@@ -2,12 +2,12 @@
 
 ## [./main.yml](./main.yml)
 
-- Triggered on pull requests into `unstable`.
+- Triggered on pull requests into `main`.
 - Our primary build and test workflow.
 
 ## [./deploy.yml](./deploy.yml)
 
-- Triggered by pull requests into `unstable`.
+- Triggered by pull requests into `main`.
 - Used for any artifacts that we deploy into production environments. Currently,
   this only consists of our website at https://apalache.informal.systems.
 
@@ -35,6 +35,6 @@
 
 ## [./container.yml](./container.yml)
 
-- Triggered by publishing releases or merging into the `unstable` branch
+- Triggered by publishing releases or merging into the `main` branch
 - The workflow builds the docker container defined in the
   [`/Dockerfile`](../../Dockerfile) and publishes it to GitHub Packages.
diff --git a/.github/workflows/auto-update.yml b/.github/workflows/auto-update.yml
index b905c8edbb..ffc33ff3c0 100644
--- a/.github/workflows/auto-update.yml
+++ b/.github/workflows/auto-update.yml
@@ -6,7 +6,7 @@ name: Auto-update
 on:
   push:
     branches:
-      - unstable
+      - main
 
 jobs:
   Auto:
diff --git a/.github/workflows/container.yml b/.github/workflows/container.yml
index bee9b0e7a9..82e24d76cf 100644
--- a/.github/workflows/container.yml
+++ b/.github/workflows/container.yml
@@ -1,5 +1,5 @@
 # This workflow builds and publishes a docker container to the GitHub registry.
-# It is only triggered on merges into the unstable branch, and we assume that
+# It is only triggered on merges into the main branch, and we assume that
 # any commit merged into the trunk has passed CI is safe to release.
 
 # Adapted from https://docs.github.com/en/actions/publishing-packages/publishing-docker-images#publishing-images-to-github-packages
@@ -12,7 +12,7 @@ on:
       - published
   push:
     branches:
-      - unstable
+      - main
 
 env:
   REGISTRY: ghcr.io
@@ -38,7 +38,7 @@ jobs:
 
       # See https://github.com/docker/metadata-action#tags-input for the default
       # tags that are extracted this way. It includes tags for semver releases
-      # and any branches into unstable
+      # and any branches into main
       - name: Extract metadata (tags, labels) for Docker
         id: meta
         uses: docker/metadata-action@98669ae865ea3cffbcbaa878cf57c20bbf1c6c38
diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml
index 04b72d8c35..c8c15e7c29 100644
--- a/.github/workflows/deploy.yml
+++ b/.github/workflows/deploy.yml
@@ -4,8 +4,8 @@ on:
   push:
     branches:
       - master
-      # TODO Remove once deploying unstable versions separately
-      - unstable
+      # TODO Remove once deploying main versions separately
+      - main
 
 jobs:
   deploy:
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 56b2176791..a8ce2f75dd 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -7,7 +7,7 @@ on:
   #  See https://github.community/t/actions-cache-cache-not-being-hit-despite-of-being-present/17956/3
   push:
     branches:
-      - unstable
+      - main
 
 name: build
 
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index f4a0a2badc..6e7433a631 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -2,7 +2,7 @@ name: release
 
 on:
   pull_request:
-    branches: [unstable]
+    branches: [main]
     types: [closed]
 
 jobs:
diff --git a/.unreleased/breaking-changes/1012-develop-on-trunk.md b/.unreleased/breaking-changes/1012-develop-on-trunk.md
new file mode 100644
index 0000000000..07c5564fc6
--- /dev/null
+++ b/.unreleased/breaking-changes/1012-develop-on-trunk.md
@@ -0,0 +1,3 @@
+Rename base development branch from `unstable` to `main`, this is noted as a
+breaking change as it could break some CI process or scripts that deploy from
+source (see #1990)
diff --git a/CHANGES.md b/CHANGES.md
index cf7e28ca45..ddc4397d9e 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -932,13 +932,13 @@
 
  * speed up by using constants instead of uninterpreted functions
 
- * options for fine tuning with `--fine-tuning`, see [tuning](https://github.com/informalsystems/apalache/blob/unstable/docs/src/apalache/tuning.md)
+ * options for fine tuning with `--fine-tuning`, see [tuning](https://github.com/informalsystems/apalache/blob/main/docs/src/apalache/tuning.md)
 
  * bugfix in logback configuration
 
 ## 0.4.0-pre1
 
- * type annotations and very simple type inference, see the [notes](https://github.com/informalsystems/apalache/blob/unstable/docs/src/apalache/types-and-annotations.md)
+ * type annotations and very simple type inference, see the [notes](https://github.com/informalsystems/apalache/blob/main/docs/src/apalache/types-and-annotations.md)
 
  * a dramatic speed up of many operators by using a `QF_NIA` theory and cherry pick
 
@@ -949,4 +949,4 @@
 
 ## 0.3.0 [RELEASE]
 
- * the version presented at the TLA+ community meeting 2018 in Oxford
\ No newline at end of file
+ * the version presented at the TLA+ community meeting 2018 in Oxford
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index b0fb6c951f..775e317265 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -91,7 +91,7 @@ to [.github/CODEOWNERS](.github/CODEOWNERS).
 
 Sometimes a contributor wants to ensure that they have a chance to review a
 [pull request](#making-a-pull-request) before the changes are landed in
-`unstable`. Contributors can lock the PR to prevent it from being merged before
+`main`. Contributors can lock the PR to prevent it from being merged before
 they can complete a review by leaving an empty review on the PR, requesting
 changes, along with a note like:
 
@@ -125,11 +125,11 @@ of landing changes:
 
 ## Making a pull request
 
-We develop on the `unstable` branch and practice [trunk-based
+We develop on the `main` branch and practice [trunk-based
 development](https://trunkbaseddevelopment.com/).
 
 Nontrivial changes should start with a [draft pull request][] against
-`unstable`. The draft signals that work is underway. When the work is ready for
+`main`. The draft signals that work is underway. When the work is ready for
 feedback, hitting "Ready for Review" will signal to the maintainers that you are
 ready for them to take a look.
 
@@ -142,7 +142,7 @@ Each stage of the process is aimed at creating feedback cycles which align
 contributors and maintainers to make sure:
 
 - Contributors don’t waste their time implementing/proposing features which
-  won’t land in `unstable`.
+  won’t land in `main`.
 - Maintainers have the necessary context in order to support and review
   contributions.
 
@@ -471,14 +471,14 @@ The process proceeds in two steps:
 Assuming the current version recorded in the project's `VERSION` file is
 `l.m.n-SNAPSHOT`, the manual release process is as follows:
 
-- [ ] `git checkout unstable && git pull`
+- [ ] `git checkout main && git pull`
 - [ ] Run `./script/release-prepare.sh` to
   - create and checkout a branch `release/l.m.n`.
   - prepare and add a release commit `[release] l.m.n`
   - update the changelog
   - bump the version number
   - commit the changes
-  - opens a pr into `unstable` with the title `[release] l.m.n`.
+  - opens a pr into `main` with the title `[release] l.m.n`.
 - [ ] Get the PR reviewed and merged and **DO NOT SQUASH THE CHANGES** on merge.
 
 If you need to set a specific version (e.g., to increment to a major version),
@@ -490,9 +490,9 @@ RELEASE_VERSION=l.m.n ./script/release-prepare.sh
 
 #### Cut the release
 
-When the PR is merged into `unstable`:
+When the PR is merged into `main`:
 
-- [ ] Checkout the `[release] l.m.n` commit from the latest `unstable`
+- [ ] Checkout the `[release] l.m.n` commit from the latest `main`
 - [ ] Run `./script/release-publish.sh` to
   - tag the release commit
   - package the
diff --git a/COORDINATION.md b/COORDINATION.md
index 362096ba82..f59d306ead 100644
--- a/COORDINATION.md
+++ b/COORDINATION.md
@@ -37,7 +37,7 @@ shared understanding of how to use and interpret the main features:
 (For more on projects vs. milestones, see
 https://stackoverflow.com/a/47542346/1187277)
 
-[adr and rfc]: https://github.com/informalsystems/apalache/tree/unstable/docs/src/adr
+[adr and rfc]: https://github.com/informalsystems/apalache/tree/main/docs/src/adr
 [discussion]: https://github.com/informalsystems/apalache/discussions
 [issues]: https://github.com/informalsystems/apalache/issues
 [labels]: https://github.com/informalsystems/apalache/issues/labels
@@ -109,7 +109,7 @@ nothing is a priority".
 
 We use a modified action-priority matrix. Our prioritization process is
 recorded in
-[RFC-21](https://github.com/informalsystems/apalache/blob/unstable/docs/src/adr/021rfc-prioritization.md)
+[RFC-21](https://github.com/informalsystems/apalache/blob/main/docs/src/adr/021rfc-prioritization.md)
 
 ### Milestones
 
diff --git a/README.md b/README.md
index 0dba874e0f..46cac42b0c 100644
--- a/README.md
+++ b/README.md
@@ -9,10 +9,10 @@ alt="Apalache Logo">
 
 </div>
 
-[![unstable badge][]][unstable-ci]
+[![main badge][]][main-ci]
 
-[unstable badge]: https://github.com/informalsystems/apalache/workflows/build/badge.svg?branch=unstable
-[unstable-ci]: https://github.com/informalsystems/apalache/actions?query=branch%3Aunstable+workflow%3Abuild
+[main badge]: https://github.com/informalsystems/apalache/workflows/build/badge.svg?branch=main
+[main-ci]: https://github.com/informalsystems/apalache/actions?query=branch%3Amain+workflow%3Abuild
 
 Apalache translates [TLA+] into the logic supported by SMT solvers such as
 [Microsoft Z3]. Apalache can check inductive invariants (for fixed or bounded
@@ -28,11 +28,11 @@ course].
 Check the [releases page][] for our latest release.
 
 For a stable release, we recommend that you pull the latest docker image with
-`docker pull ghcr.io/informalsystems/apalache:unstable`, use the jar from the
+`docker pull ghcr.io/informalsystems/apalache:main`, use the jar from the
 most recent release, or checkout the source code from the most recent release
 tag.
 
-To try the latest cool features, check out the head of the [unstable branch][].
+To try the latest cool features, check out the head of the [main branch][].
 
 For more information on installation options, see [the
 manual][user-manual-installation].
@@ -144,7 +144,7 @@ Past funding from [Der Wiener Wissenschafts-, Forschungs- und Technologiefonds](
 [video course]: http://lamport.azurewebsites.net/video/videos.html
 [releases page]: https://github.com/informalsystems/apalache/releases
 [master]: https://github.com/informalsystems/apalache/tree/master
-[unstable branch]: https://github.com/informalsystems/apalache/tree/unstable
+[main branch]: https://github.com/informalsystems/apalache/tree/main
 [apalache zulip stream]: https://informal-systems.zulipchat.com/#narrow/stream/265309-apalache
 [tendermint specs]: https://github.com/tendermint/tendermint/tree/master/spec/light-client/accountability
 [tendermint blockchain]: https://github.com/tendermint
diff --git a/build.sbt b/build.sbt
index a9e98dfb94..0e1d3f8503 100644
--- a/build.sbt
+++ b/build.sbt
@@ -76,7 +76,7 @@ ThisBuild / scalacOptions ++= {
 // scalafmt
 // TODO: Remove if we decide we are happy with allways reformatting all
 // Only check/fix against (tracked) files that have changed relative to the trunk
-// ThisBuild / scalafmtFilter := "diff-ref=origin/unstable"
+// ThisBuild / scalafmtFilter := "diff-ref=origin/main"
 ThisBuild / scalafmtPrintDiff := true
 
 // scalafix
diff --git a/docs/highlightjs-tlaplus/package.json b/docs/highlightjs-tlaplus/package.json
index ad6637671e..b98dd056a1 100644
--- a/docs/highlightjs-tlaplus/package.json
+++ b/docs/highlightjs-tlaplus/package.json
@@ -14,7 +14,7 @@
   "bugs": {
     "url": "https://github.com/informalsystems/apalache/issues"
   },
-  "homepage": "https://github.com/informalsystems/apalache/tree/unstable/docs/highlightjs-tlaplus",
+  "homepage": "https://github.com/informalsystems/apalache/tree/main/docs/highlightjs-tlaplus",
   "devDependencies": {
     "highlight.js": "^11.5.1"
   }
diff --git a/docs/src/HOWTOs/howto-write-type-annotations.md b/docs/src/HOWTOs/howto-write-type-annotations.md
index 229354ad77..75477652d4 100644
--- a/docs/src/HOWTOs/howto-write-type-annotations.md
+++ b/docs/src/HOWTOs/howto-write-type-annotations.md
@@ -504,7 +504,7 @@ This may change later, when the tlaplus [Issue 578][] is resolved.
 
 
 [old type annotations]: ../apalache/types-and-annotations.md
-[Apalache.tla]: https://github.com/informalsystems/apalache/blob/unstable/src/tla/Apalache.tla
+[Apalache.tla]: https://github.com/informalsystems/apalache/blob/main/src/tla/Apalache.tla
 [Snowcat]: ../apalache/typechecker-snowcat.md
 [ADR002]: ../adr/002adr-types.md
 [HourClock.tla]: https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/RealTime/HourClock.tla
@@ -518,7 +518,7 @@ This may change later, when the tlaplus [Issue 578][] is resolved.
 [Issue 578]: https://github.com/tlaplus/tlaplus/issues/578
 [Issue 718]: https://github.com/informalsystems/apalache/issues/718
 [MissionariesAndCannibals.tla]: https://github.com/tlaplus/Examples/blob/master/specifications/MissionariesAndCannibals/MissionariesAndCannibals.tla
-[Variants module]: https://github.com/informalsystems/apalache/blob/unstable/src/tla/Variants.tla
+[Variants module]: https://github.com/informalsystems/apalache/blob/main/src/tla/Variants.tla
 [Chapter on variants]: ../lang/variants.md
 [Idiom 3]: ../idiomatic/003record-sets.md
 [LamportMutex.tla]: https://github.com/tlaplus/Examples/blob/master/specifications/lamport_mutex/LamportMutex.tla
diff --git a/docs/src/adr/002adr-types.md b/docs/src/adr/002adr-types.md
index 8446bc4ef3..d1e1617ced 100644
--- a/docs/src/adr/002adr-types.md
+++ b/docs/src/adr/002adr-types.md
@@ -549,8 +549,8 @@ AtMostOne ==
 
 [Snowcat tutorial]: https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html
 [Snowcat HOWTO]: https://apalache.informal.systems/docs/HOWTOs/howto-write-type-annotations.html
-[ADR014]: https://github.com/informalsystems/apalache/blob/unstable/docs/src/adr/014adr-precise-records.md
+[ADR014]: https://github.com/informalsystems/apalache/blob/main/docs/src/adr/014adr-precise-records.md
 [Issue 401]: https://github.com/informalsystems/apalache/issues/401
 [Row polymorphism]: https://en.wikipedia.org/wiki/Row_polymorphism
-[Variants.tla]: https://github.com/informalsystems/apalache/blob/unstable/src/tla/Variants.tla
+[Variants.tla]: https://github.com/informalsystems/apalache/blob/main/src/tla/Variants.tla
 [variant types]: https://en.wikipedia.org/wiki/Tagged_union
diff --git a/docs/src/adr/004adr-annotations.md b/docs/src/adr/004adr-annotations.md
index 9094f4bed1..0986b8a60c 100644
--- a/docs/src/adr/004adr-annotations.md
+++ b/docs/src/adr/004adr-annotations.md
@@ -163,5 +163,5 @@ so it would be otherwise impossible to find the end of an annotation.
 
 [Java identifier]: https://docs.oracle.com/javase/specs/jls/se7/html/jls-3.html#jls-3.8
 
-[AnnotationParser]: https://github.com/informalsystems/apalache/blob/unstable/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/AnnotationParser.scala
+[AnnotationParser]: https://github.com/informalsystems/apalache/blob/main/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/AnnotationParser.scala
 
diff --git a/docs/src/adr/005adr-json.md b/docs/src/adr/005adr-json.md
index 36a68d1133..cabe455e39 100644
--- a/docs/src/adr/005adr-json.md
+++ b/docs/src/adr/005adr-json.md
@@ -205,7 +205,7 @@ The implementation of the serialization can be found in the class
 
 [ADR-004]: https://apalache.informal.systems/docs/adr/004adr-annotations.html
 
-[TlaToJson]: https://github.com/informalsystems/apalache/blob/unstable/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala#L54
-[TlaEx]: https://github.com/informalsystems/apalache/blob/unstable/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaEx.scala#L10
-[TlaDecl]: https://github.com/informalsystems/apalache/blob/unstable/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDecl.scala#L9
-[TlaModule]: https://github.com/informalsystems/apalache/blob/unstable/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDecl.scala#L19
+[TlaToJson]: https://github.com/informalsystems/apalache/blob/main/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala#L54
+[TlaEx]: https://github.com/informalsystems/apalache/blob/main/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaEx.scala#L10
+[TlaDecl]: https://github.com/informalsystems/apalache/blob/main/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDecl.scala#L9
+[TlaModule]: https://github.com/informalsystems/apalache/blob/main/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDecl.scala#L19
diff --git a/docs/src/adr/006rfc-unit-testing.md b/docs/src/adr/006rfc-unit-testing.md
index 31e4b5393b..a16a24e023 100644
--- a/docs/src/adr/006rfc-unit-testing.md
+++ b/docs/src/adr/006rfc-unit-testing.md
@@ -634,7 +634,7 @@ Let us know:
 [Property-based testing]: https://en.wikipedia.org/wiki/QuickCheck
 [TLA+ examples]: https://github.com/tlaplus/Examples/
 [LCR]: https://github.com/tlaplus/Examples/tree/master/specifications/chang_roberts
-[ChangRobertsTyped_Test.tla]: https://github.com/informalsystems/apalache/blob/unstable/test/tla/ChangRobertsTyped_Test.tla
+[ChangRobertsTyped_Test.tla]: https://github.com/informalsystems/apalache/blob/main/test/tla/ChangRobertsTyped_Test.tla
 [Distributed Algorithms]: https://dl.acm.org/doi/book/10.5555/2821576
 [Raft]: https://github.com/tlaplus/Examples/tree/master/specifications/raft
 [Apalache.tla]: https://github.com/informalsystems/apalache/blob/80cf914fe7272b14832a47b21193f5dfe8119348/src/tla/Apalache.tla
diff --git a/docs/src/adr/010rfc-transition-explorer.md b/docs/src/adr/010rfc-transition-explorer.md
index 00969e1122..584848503a 100644
--- a/docs/src/adr/010rfc-transition-explorer.md
+++ b/docs/src/adr/010rfc-transition-explorer.md
@@ -153,7 +153,7 @@ I propose the following high-level architecture:
 *NOTE*: The high-level sketch above assumes the new code organization proposed
 in [ADR 7][].
 
-[ADR 7]: https://github.com/informalsystems/apalache/tree/unstable/docs/src/adr/007adr-restructuring.md
+[ADR 7]: https://github.com/informalsystems/apalache/tree/main/docs/src/adr/007adr-restructuring.md
 
 #### API
 
@@ -170,7 +170,7 @@ with `Example`.
 
 In essence, this proposed API is only a thin wrapper around the
 [TransitionExecutor
-class](https://github.com/informalsystems/apalache/tree/unstable/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutor.scala).
+class](https://github.com/informalsystems/apalache/tree/main/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutor.scala).
 During previous iterations of the proposed API we discussed exposing a
 higher-level API, targeted at meeting the requirements more directly.  However,
 discussion revealed that the expensive computational costs of SAT solving in
diff --git a/docs/src/adr/015adr-trace.md b/docs/src/adr/015adr-trace.md
index d4b10f3c85..ce615f2d5a 100644
--- a/docs/src/adr/015adr-trace.md
+++ b/docs/src/adr/015adr-trace.md
@@ -446,6 +446,6 @@ Reserved for the future.
 
 
 [ADR005]: https://apalache.informal.systems/docs/adr/005adr-json.html
-[MissionariesAndCannibalsTyped]: https://github.com/informalsystems/apalache/blob/unstable/test/tla/MissionariesAndCannibalsTyped.tla
+[MissionariesAndCannibalsTyped]: https://github.com/informalsystems/apalache/blob/main/test/tla/MissionariesAndCannibalsTyped.tla
 [JSON]: https://en.wikipedia.org/wiki/JSON
 [RFC7159]: https://datatracker.ietf.org/doc/html/rfc7159.html
diff --git a/docs/src/apalache/assignments-in-depth.md b/docs/src/apalache/assignments-in-depth.md
index 4e899f9273..04a51754b8 100644
--- a/docs/src/apalache/assignments-in-depth.md
+++ b/docs/src/apalache/assignments-in-depth.md
@@ -75,7 +75,7 @@ that has one of the following forms:
 - `x' = e`,
 - `x' \in S`,
 - `UNCHANGED x`, or
-- `x' := e` (note that `:=` is the operator defined in [Apalache.tla](https://github.com/informalsystems/apalache/blob/unstable/src/tla/Apalache.tla))
+- `x' := e` (note that `:=` is the operator defined in [Apalache.tla](https://github.com/informalsystems/apalache/blob/main/src/tla/Apalache.tla))
 
 So to reformulate the second requirement: the transition operator must contain
 at least one assignment candidate for each variable declared in the
diff --git a/docs/src/apalache/example.md b/docs/src/apalache/example.md
index 9a96e1b417..83b5b7d6e3 100644
--- a/docs/src/apalache/example.md
+++ b/docs/src/apalache/example.md
@@ -2,7 +2,7 @@
 
 We introduce a TLA+ specification that we use to discuss features of Apalache in
 the following sections. Its source code can be found in
-[`test/tla/y2k.tla`](https://github.com/informalsystems/apalache/blob/unstable/test/tla/y2k.tla):
+[`test/tla/y2k.tla`](https://github.com/informalsystems/apalache/blob/main/test/tla/y2k.tla):
 
 ```tla
 {{#include ../../../test/tla/y2k.tla::55}}
diff --git a/docs/src/apalache/installation/docker.md b/docs/src/apalache/installation/docker.md
index 7f9590450d..56c17f620b 100644
--- a/docs/src/apalache/installation/docker.md
+++ b/docs/src/apalache/installation/docker.md
@@ -39,7 +39,7 @@ The following docker parameters are used:
   When using SELinux, you might have to use the modified form of `-v` option:
     `-v <your-spec-directory>:/var/apalache:z`
 - `informalsystems/apalache` is the APALACHE docker image name. By default, the `latest` stable
-  version is used; you can also refer to a specific tool version, e.g., `informalsystems/apalache:0.6.0` or `informalsystems/apalache:unstable`
+  version is used; you can also refer to a specific tool version, e.g., `informalsystems/apalache:0.6.0` or `informalsystems/apalache:main`
 - `<args>` are the tool arguments as described in [Running the Tool](../running.md).
 
 We provide a convenience wrapper for this docker command in
@@ -69,42 +69,44 @@ Apalache in docker while sharing the working directory:
 
 $ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/informalsystems/apalache'
 
-###### using the latest unstable
+###### using the latest main
 
-$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/informalsystems/apalache:unstable'
+$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/informalsystems/apalache:main'
 ```
 
-## Using the unstable version of Apalache
+## Using the development branch of Apalache
 
-The development of Apalache proceeds at a high pace, and we introduce a
-substantial number of improvements in the unstable branch before the next stable
-release. Please refer to the [change
-log](https://github.com/informalsystems/apalache/blob/unstable/CHANGES.md) and
-[manual](https://github.com/informalsystems/apalache/blob/unstable/docs/src/apalache/index.md)
-on the unstable branch for the description of the newest features. **We
-recommend using the unstable version if you want to try all the exciting new
-features of Apalache. But be warned: It is called "unstable" for a reason**. To
-use `unstable`, just type `ghcr.io/informalsystems/apalache:unstable` instead of `ghcr.io/informalsystems/apalache`
-everywhere.
+The development of Apalache proceeds at a quick pace and we cut releases weekly.
+Please refer to the [changelog][] and the [manual][] on the `main` development
+branch for a report of the newest features. Since we cut releases weekly, you
+should have access to all the latest features in the last week by using the
+`latest` tag. However, if you wish to use the very latest developments as they
+are added throughout the week, you can run the image with the `main` tag: just
+type `ghcr.io/informalsystems/apalache:main` instead of
+`ghcr.io/informalsystems/apalache` everywhere.
 
 Do not forget to pull the docker image from time to time:
 
 ```bash
-docker pull ghcr.io/informalsystems/apalache:unstable
+docker pull ghcr.io/informalsystems/apalache:main
 ```
 
 Run it with the following command:
 
 ```bash
-$ docker run --rm -v <your-spec-directory>:/var/apalache ghcr.io/informalsystems/apalache:unstable <args>
+$ docker run --rm -v <your-spec-directory>:/var/apalache ghcr.io/informalsystems/apalache:main <args>
 ```
 
-To create an alias pointing to the `unstable` version:
+To create an alias pointing to the `main` version:
 
 ```bash
-$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/informalsystems/apalache:unstable'
+$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/informalsystems/apalache:main'
 ```
 
+[changelog]: https://github.com/informalsystems/apalache/blob/main/CHANGES.md
+[manual]: https://github.com/informalsystems/apalache/blob/main/docs/src/apalache/index.md
+
+
 ## Building an image
 
 For an end user there is no need to build an Apalache image. If you like to
diff --git a/docs/src/apalache/installation/jvm.md b/docs/src/apalache/installation/jvm.md
index b3897382ec..f704b6b9d2 100644
--- a/docs/src/apalache/installation/jvm.md
+++ b/docs/src/apalache/installation/jvm.md
@@ -20,7 +20,7 @@ better, add the `./bin` directory to your `PATH` and run `apalache-mc`.
 
 If you would like to contribute a command-line script for running Apalache in
 Windows, please [open a pull
-request](https://github.com/informalsystems/apalache/blob/unstable/CONTRIBUTING.md#making-a-pull-request).
+request](https://github.com/informalsystems/apalache/blob/main/CONTRIBUTING.md#making-a-pull-request).
 
 [Eclipse Temurin]: https://adoptium.net/
 [Zulu]: https://www.azul.com/downloads/?version=java-17-lts&package=jdk#download-openjdk
diff --git a/docs/src/apalache/installation/source.md b/docs/src/apalache/installation/source.md
index a8933463c4..ad99a64f1a 100644
--- a/docs/src/apalache/installation/source.md
+++ b/docs/src/apalache/installation/source.md
@@ -37,4 +37,4 @@ repository, you have three options after running `make`:
 [compatibility table]: https://docs.scala-lang.org/overviews/jdk-compatibility/overview.html
 [sbt]: https://www.scala-sbt.org/1.x/docs/Setup.html
 [direnv]: https://direnv.net/
-[shell environment]: https://github.com/informalsystems/apalache/blob/unstable/CONTRIBUTING.md#environment
+[shell environment]: https://github.com/informalsystems/apalache/blob/main/CONTRIBUTING.md#environment
diff --git a/docs/src/apalache/parameters.md b/docs/src/apalache/parameters.md
index 174f531d95..075e70a988 100644
--- a/docs/src/apalache/parameters.md
+++ b/docs/src/apalache/parameters.md
@@ -8,7 +8,7 @@ by writing a symbolic constraint, see [Section 5.3](#ConstInit).
 
 You can set the specification parameters, using the standard `INSTANCE`
 expression of TLA+. For instance, below is the example
-[`y2k_instance.tla`](https://github.com/informalsystems/apalache/blob/unstable/test/tla/y2k_instance.tla),
+[`y2k_instance.tla`](https://github.com/informalsystems/apalache/blob/main/test/tla/y2k_instance.tla),
 which instantiates `y2k.tla`:
 
 ```tla
@@ -33,7 +33,7 @@ Alternatively, you can extend the base module and use overrides:
 This approach is similar to the ``Init`` operator, but applied to the
 constants. We define a special operator, e.g., called ``ConstInit``. For
 instance, below is the example
-[`y2k_cinit.tla`](https://github.com/informalsystems/apalache/blob/unstable/test/tla/y2k_cinit.tla):
+[`y2k_cinit.tla`](https://github.com/informalsystems/apalache/blob/main/test/tla/y2k_cinit.tla):
 
 ```tla
 {{#include ../../../test/tla/y2k_cinit.tla::13}}
diff --git a/docs/src/apalache/principles/apalache-mod.md b/docs/src/apalache/principles/apalache-mod.md
index e76343fb8b..cdf3df6dd8 100644
--- a/docs/src/apalache/principles/apalache-mod.md
+++ b/docs/src/apalache/principles/apalache-mod.md
@@ -7,6 +7,6 @@ the [detailed output](./running.md#detailed) produced by the tool.
 
 See the detailed description of the [Apalache operators][].
 
-[Apalache.tla]: https://github.com/informalsystems/apalache/tree/unstable/src/tla/Apalache.tla
+[Apalache.tla]: https://github.com/informalsystems/apalache/tree/main/src/tla/Apalache.tla
 
 [Apalache operators]: https://apalache.informal.systems/docs/lang/apalache-operators.html
diff --git a/docs/src/apalache/principles/assignments.md b/docs/src/apalache/principles/assignments.md
index d37c78c465..035a765a89 100644
--- a/docs/src/apalache/principles/assignments.md
+++ b/docs/src/apalache/principles/assignments.md
@@ -3,9 +3,9 @@
 ## Assignments and symbolic transitions
 
 Let us go back to the example
-[`test/tla/y2k.tla`](https://github.com/informalsystems/apalache/blob/unstable/test/tla/y2k.tla)
+[`test/tla/y2k.tla`](https://github.com/informalsystems/apalache/blob/main/test/tla/y2k.tla)
 and run `apalache-mc` against
-[`test/tla/y2k_override.tla`](https://github.com/informalsystems/apalache/blob/unstable/test/tla/y2k_override.tla)
+[`test/tla/y2k_override.tla`](https://github.com/informalsystems/apalache/blob/main/test/tla/y2k_override.tla)
 while instructing Apalache to write intermediate output files:
 
 ```console
@@ -53,7 +53,7 @@ follows:
 
 If Apalache cannot find expressions with the above properties, it fails.
 Consider the example
-[`test/tla/Assignments20200309.tla`](https://github.com/informalsystems/apalache/blob/unstable/test/tla/Assignments20200309.tla):
+[`test/tla/Assignments20200309.tla`](https://github.com/informalsystems/apalache/blob/main/test/tla/Assignments20200309.tla):
 
 ```tla
 {{#include ../../../../test/tla/Assignments20200309.tla::}}
diff --git a/docs/src/apalache/statistics.md b/docs/src/apalache/statistics.md
index 50e1d369e3..42ff51cd1b 100644
--- a/docs/src/apalache/statistics.md
+++ b/docs/src/apalache/statistics.md
@@ -72,7 +72,7 @@ The following data is submitted for each run, if you have opted in:
 [Visual Studio Code Plugin for TLA+]: https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus
 [anonymized statistics programme]: https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/util/ExecutionStatisticsCollector.md
 [ExecutionStatisticsCollector]: https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/util/ExecutionStatisticsCollector.java
-[Tool]: https://github.com/informalsystems/apalache/blob/unstable/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala
+[Tool]: https://github.com/informalsystems/apalache/blob/main/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala
 [Informal Systems]: https://informal.systems
 [TU Wien]: https://www.tuwien.at/
 [Vienna Science and Technology Fund]: https://www.wwtf.at/index.php?lang=EN
diff --git a/docs/src/lang/sequences.md b/docs/src/lang/sequences.md
index 2bf3976a72..bbedf8425d 100644
--- a/docs/src/lang/sequences.md
+++ b/docs/src/lang/sequences.md
@@ -577,7 +577,7 @@ till the end of the universe.
 [Control Flow and Non-determinism]: ./control-and-nondeterminism.md
 [Specifying Systems]: http://lamport.azurewebsites.net/tla/book.html?back-link=learning.html
 [Paxos]: https://github.com/tlaplus/Examples/blob/master/specifications/Paxos/Paxos.tla
-[Apalache ADR002]: https://github.com/informalsystems/apalache/blob/unstable/docs/src/adr/002adr-types.md
+[Apalache ADR002]: https://github.com/informalsystems/apalache/blob/main/docs/src/adr/002adr-types.md
 [Cartesian product]: https://en.wikipedia.org/wiki/Cartesian_product
 [Overriding Seq in TLC]: https://groups.google.com/g/tlaplus/c/sYx_6e3YyWk/m/4CnwPqIVAgAJ
 [HOWTO write type annotations]: ../../HOWTOs/howto-write-type-annotations.md
diff --git a/docs/src/lang/variants.md b/docs/src/lang/variants.md
index 1470679d28..879df94b52 100644
--- a/docs/src/lang/variants.md
+++ b/docs/src/lang/variants.md
@@ -369,4 +369,4 @@ IN
 
 [Variants]: https://en.wikipedia.org/wiki/Tagged_union
 [Tagged unions in Paxos]: https://github.com/tlaplus/Examples/blob/779852ba9951621f062fc4074b8e81fd12db21dc/specifications/Paxos/Paxos.tla#L85-L106
-[Variants.tla]: https://github.com/informalsystems/apalache/blob/unstable/src/tla/Variants.tla
+[Variants.tla]: https://github.com/informalsystems/apalache/blob/main/src/tla/Variants.tla
diff --git a/docs/src/tutorials/entry-tutorial.md b/docs/src/tutorials/entry-tutorial.md
index 9ce520a327..c7cd9a712c 100644
--- a/docs/src/tutorials/entry-tutorial.md
+++ b/docs/src/tutorials/entry-tutorial.md
@@ -96,7 +96,7 @@ reasons for that:
 ## Step 0: Introducing a template module
 
 *Source files for this step*:
-[BinSearch0.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch0.tla).
+[BinSearch0.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch0.tla).
 
 TLA+ is built around the concept of a state machine. The specified system
 starts in a state that is picked from the set of its *initial states*. This
@@ -164,9 +164,9 @@ that the tools are working.
 ## Step 1: Introducing specification parameters
 
 *Source files for this step*:
-[BinSearch1.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch1.tla).
+[BinSearch1.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch1.tla).
 
-*Diffs*: [BinSearch1.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch1.tla.patch).
+*Diffs*: [BinSearch1.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch1.tla.patch).
 
 The Java code of `binarySearch` accepts two parameters: an array of integers
 called `a`, and an integer called `key`. Similar to these parameters, we introduce
@@ -219,9 +219,9 @@ $ apalache-mc check BinSearch1.tla
 ## Step 2: Specifying the base case
 
 *Source files for this step*:
-[BinSearch2.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch2.tla).
+[BinSearch2.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch2.tla).
 
-*Diffs*: [BinSearch2.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch2.tla.patch).
+*Diffs*: [BinSearch2.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch2.tla.patch).
 
 We start with the simplest possible case that occurs in `binarySearch`. Namely,
 we consider the case where `low > high`, that is, `binarySearch` never enters
@@ -358,9 +358,9 @@ being delayed until the whole predicate `Next` is evaluated.
 ## Step 2b: Basic checks for the base case
 
 *Source files for this step*:
-[BinSearch2.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch2.tla)
+[BinSearch2.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch2.tla)
 and
-[MC2_8.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC2_8.tla).
+[MC2_8.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC2_8.tla).
 
 As we discussed, it is a good habit to periodically run the model checker, as you are writing
 the specification. Even if it doesn't check much, you would be able to catch
@@ -427,14 +427,14 @@ expectations yet!
 ## Step 3: Specifying an invariant and checking it for the base case
 
 *Source files for this step*:
-[BinSearch3.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch3.tla)
+[BinSearch3.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch3.tla)
 and
-[MC3_8.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC3_8.tla).
+[MC3_8.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC3_8.tla).
 
 *Diffs*:
-[BinSearch3.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch3.tla.patch)
+[BinSearch3.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch3.tla.patch)
 and
-[MC3_8.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC3_8.tla.patch).
+[MC3_8.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC3_8.tla.patch).
 
 What do we expect from binary search? We can check the Java documentation,
 e.g., [Arrays.java in OpenJDK][]:
@@ -519,14 +519,14 @@ Step 5, we will check `Postcondition` for all sequences admitted by `INT_WIDTH`.
 ## Step 4: Specifying the loop (with a caveat)
 
 *Source files for this step*:
-[BinSearch4.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch4.tla)
+[BinSearch4.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch4.tla)
 and
-[MC4_8.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC4_8.tla).
+[MC4_8.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC4_8.tla).
 
 *Diffs*:
-[BinSearch4.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch4.tla.patch)
+[BinSearch4.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch4.tla.patch)
 and
-[MC4_8.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC4_8.tla.patch).
+[MC4_8.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC4_8.tla.patch).
 
 We specify the loop of `binarySearch` in TLA+ as follows:
 
@@ -617,14 +617,14 @@ a detailed explanation in the section on [Assignments in Apalache][].
 ## Step 5: Checking Postcondition for plenty of inputs
 
 *Source files for this step*:
-[BinSearch5.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch5.tla)
+[BinSearch5.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch5.tla)
 and
-[MC5_8.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC5_8.tla).
+[MC5_8.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC5_8.tla).
 
 *Diffs*:
-[BinSearch5.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch5.tla.patch)
+[BinSearch5.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch5.tla.patch)
 and
-[MC5_8.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC5_8.tla.patch).
+[MC5_8.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC5_8.tla.patch).
 
 In this step, we are going to check the invariant `Postcondition` for all
 possible input sequences and all input keys (for a fixed bit-width).
@@ -761,9 +761,9 @@ the search, rather our invariant `Postcondition` is imprecise.
 ## Step 5b: Fixing the postcondition
 
 *Source files for this step*:
-[BinSearch5.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch5.tla)
+[BinSearch5.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch5.tla)
 and
-[MC5_8.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC5_8.tla).
+[MC5_8.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC5_8.tla).
 
 If we check our source of truth, that is, the Java documentation in
 [Arrays.java in OpenJDK][], we will see the following sentences:
@@ -810,14 +810,14 @@ whether the search is terminating on all inputs.
 ## Step 6: Checking termination and progress
 
 *Source files for this step*:
-[BinSearch6.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch6.tla)
+[BinSearch6.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch6.tla)
 and
-[MC6_8.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC6_8.tla).
+[MC6_8.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC6_8.tla).
 
 *Diffs*:
-[BinSearch6.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch6.tla.patch)
+[BinSearch6.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch6.tla.patch)
 and
-[MC6_8.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC6_8.tla.patch).
+[MC6_8.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC6_8.tla.patch).
 
 Actually, we do not need 10 steps to check termination for the case `INT_WIDTH
 = 8`. If you recall the complexity of the binary search, it needs
@@ -886,14 +886,14 @@ It takes about 10 seconds to check `Progress` as well.
 ## Step 7: Fixed-width integers
 
 *Source files for this step*:
-[BinSearch7.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch7.tla)
+[BinSearch7.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch7.tla)
 and
-[MC7_8.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC7_8.tla).
+[MC7_8.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC7_8.tla).
 
 *Diffs*:
-[BinSearch7.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch7.tla.patch)
+[BinSearch7.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch7.tla.patch)
 and
-[MC7_8.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC7_8.tla.patch).
+[MC7_8.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC7_8.tla.patch).
 
 Do you recall that our specification of the loop had a caveat? Let us have a
 look at this piece of the specification again:
@@ -955,14 +955,14 @@ issue that is caused by the integer overflow!
 ## Step 8: Checking the boundaries
 
 *Source files for this step*:
-[BinSearch8.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch8.tla)
+[BinSearch8.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch8.tla)
 and
-[MC8_8.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC8_8.tla).
+[MC8_8.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC8_8.tla).
 
 *Diffs*:
-[BinSearch8.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch8.tla.patch)
+[BinSearch8.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch8.tla.patch)
 and
-[MC8_8.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC8_8.tla.patch).
+[MC8_8.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC8_8.tla.patch).
 
 As we have seen in Step 7, the cause of all errors in `PostconditionSorted`,
 `Termination`, and `Progress` is that the addition `low + high` overflows and
@@ -1018,14 +1018,14 @@ In state 1, we have `low + high = 116 + 59 > 2^7`. Since we have `INT_WIDTH
 ## Step 9: Fixing the access bug
 
 *Source files for this step*:
-[BinSearch9.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch9.tla)
+[BinSearch9.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch9.tla)
 and
-[MC9_8.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC9_8.tla).
+[MC9_8.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC9_8.tla).
 
 *Diffs*:
-[BinSearch9.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch9.tla.patch)
+[BinSearch9.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch9.tla.patch)
 and
-[MC9_8.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC9_8.tla.patch).
+[MC9_8.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC9_8.tla.patch).
 
 Let us apply the fix that was proposed by Joshua Bloch in [Nearly All Binary
 Searches and Mergesorts are Broken][]. Namely, we update this line of
@@ -1093,14 +1093,14 @@ Observe that it takes Apalache significantly more time.
 ## Step 10: Beautifying the specification
 
 *Source files for this step*:
-[BinSearch10.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch10.tla)
+[BinSearch10.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch10.tla)
 and
-[MC10_8.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC10_8.tla).
+[MC10_8.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC10_8.tla).
 
 *Diffs*:
-[BinSearch10.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch10.tla.patch)
+[BinSearch10.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch10.tla.patch)
 and
-[MC10_8.tla.patch](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC10_8.tla.patch).
+[MC10_8.tla.patch](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC10_8.tla.patch).
 
 We have reached our goals: TLA+ and Apalache helped us in finding the access
 bug and showing that its fix works. Now it is time to look back at the
@@ -1127,9 +1127,9 @@ variables.
 ## Discussion
 
 The final specifications can be found in
-[BinSearch10.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/BinSearch10.tla)
+[BinSearch10.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch10.tla)
 and
-[MC10_8.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bin-search/MC10_8.tla).
+[MC10_8.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/MC10_8.tla).
 
 In this tutorial we have shown how to:
 
diff --git a/docs/src/tutorials/pluscal-tutorial.md b/docs/src/tutorials/pluscal-tutorial.md
index 5c63e28e0c..e605267145 100644
--- a/docs/src/tutorials/pluscal-tutorial.md
+++ b/docs/src/tutorials/pluscal-tutorial.md
@@ -239,9 +239,9 @@ IsPositive(x) == x > 0
 ## Conclusion
 
 The final specifications can be found in
-[BakeryTyped.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bakery-pluscal/BakeryTyped.tla)
+[BakeryTyped.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bakery-pluscal/BakeryTyped.tla)
 and
-[BakeryWoTlaps.tla](https://github.com/informalsystems/apalache/blob/unstable/test/tla/bakery-pluscal/BakeryWoTlaps.tla).
+[BakeryWoTlaps.tla](https://github.com/informalsystems/apalache/blob/main/test/tla/bakery-pluscal/BakeryWoTlaps.tla).
 
 In this tutorial we have shown how to:
 
@@ -264,7 +264,7 @@ or drop us a message on [Zulip chat].
 
 [PlusCal specification]: https://github.com/tlaplus/Examples/blob/master/specifications/Bakery-Boulangerie/Bakery.tla
 [Bakery.tla]: https://github.com/tlaplus/Examples/blob/master/specifications/Bakery-Boulangerie/Bakery.tla
-[BakeryWoTlaps.tla]: https://github.com/informalsystems/apalache/blob/unstable/test/tla/bakery-pluscal/BakeryWoTlaps.tla
+[BakeryWoTlaps.tla]: https://github.com/informalsystems/apalache/blob/main/test/tla/bakery-pluscal/BakeryWoTlaps.tla
 [Entry-level Tutorial on the Model Checker]: ./entry-tutorial.md
 [HOWTO on writing type annotations]: ../HOWTOs/howto-write-type-annotations.md
 [Apalache installation]: ../apalache/installation/index.md
diff --git a/docs/src/tutorials/snowcat-tutorial.md b/docs/src/tutorials/snowcat-tutorial.md
index bd86b1eadd..7cd5651302 100644
--- a/docs/src/tutorials/snowcat-tutorial.md
+++ b/docs/src/tutorials/snowcat-tutorial.md
@@ -311,8 +311,8 @@ or drop us a message on [Zulip chat][].
 [Lamport's mutex]: https://github.com/tlaplus/Examples/blob/master/specifications/lamport_mutex
 [TwoPhase.tla]: https://github.com/tlaplus/Examples/blob/911dac1462344337940779a797a5f329a77be98c/specifications/transaction_commit/TwoPhase.tla
 [LamportMutex.tla]: https://github.com/tlaplus/Examples/blob/master/specifications/lamport_mutex/LamportMutex.tla
-[LamportMutexTyped.tla]: https://github.com/informalsystems/apalache/blob/unstable/test/tla/LamportMutexTyped.tla
-[TwoPhaseTyped.tla]: https://github.com/informalsystems/apalache/blob/unstable/test/tla/TwoPhaseTyped.tla
+[LamportMutexTyped.tla]: https://github.com/informalsystems/apalache/blob/main/test/tla/LamportMutexTyped.tla
+[TwoPhaseTyped.tla]: https://github.com/informalsystems/apalache/blob/main/test/tla/TwoPhaseTyped.tla
 [Stephan Merz]: https://members.loria.fr/Stephan.Merz/
 [GameOfLifeTyped.tla]: https://github.com/informalsystems/apalache/blob/d5138a33fce3d77abc07a39bfb4f448942e6f641/test/tla/GameOfLifeTyped.tla 
 [CigaretteSmokersTyped.tla]: https://github.com/informalsystems/apalache/blob/d5138a33fce3d77abc07a39bfb4f448942e6f641/test/tla/CigaretteSmokersTyped.tla
diff --git a/script/latest-message.txt b/script/latest-message.txt
index ac06d5120d..7bb0280075 100644
--- a/script/latest-message.txt
+++ b/script/latest-message.txt
@@ -1,3 +1,3 @@
-This is the latest successful build of the unstable branch, which contains cool
+This is the latest successful build of the main branch, which contains cool
 new features but is not guaranteed to work. If you want to experiment, this
 build is for you.
diff --git a/script/release-prepare.sh b/script/release-prepare.sh
index e19b220479..3d623dcbef 100755
--- a/script/release-prepare.sh
+++ b/script/release-prepare.sh
@@ -72,7 +72,7 @@ instructions="
 # Reviewer instructions
 
 - Check the changelog to ensure the version increment is consistent with https://semver.org/.
-  - If a different version should be released, follow [the instructions](https://github.com/informalsystems/apalache/blob/unstable/CONTRIBUTING.md#via-github).
+  - If a different version should be released, follow [the instructions](https://github.com/informalsystems/apalache/blob/main/CONTRIBUTING.md#via-github).
 - Review the changeset as a sanity check.
 - Approve the PR, if it pases muster.
 - **Merge** this branch (do not squash or rebase), but **DO NOT DELETE THE BRANCH**.
@@ -91,4 +91,4 @@ hub pull-request \
     --message="$commit_msg" \
     --message="$instructions" \
     --message="$body" \
-    --base="unstable"
+    --base="main"
diff --git a/src/tla/Apalache.tla b/src/tla/Apalache.tla
index ca73d46da3..b8bb5cb1c5 100644
--- a/src/tla/Apalache.tla
+++ b/src/tla/Apalache.tla
@@ -24,7 +24,7 @@
  * assignments by hand, you can use this operator.
  *
  * For a further discussion on that matter, see:
- * https://github.com/informalsystems/apalache/blob/unstable/docs/src/idiomatic/001assignments.md
+ * https://github.com/informalsystems/apalache/blob/main/docs/src/idiomatic/001assignments.md
  *)
 __x := __e == __x = __e
 
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala
index 16b6ba2e2d..cd61266210 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala
@@ -10,7 +10,7 @@ sealed trait Feature {
 
 /**
  * Enable rows, new records, and variants, as described in <a
- * href="https://github.com/informalsystems/apalache/blob/unstable/docs/src/adr/014adr-precise-records.md">ADR-014</a>.
+ * href="https://github.com/informalsystems/apalache/blob/main/docs/src/adr/014adr-precise-records.md">ADR-014</a>.
  */
 case class RowsFeature(
     name: String = "rows",
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaType1.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaType1.scala
index 76058d8a6f..c0f29ac14d 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaType1.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaType1.scala
@@ -4,10 +4,10 @@ import scala.collection.immutable.SortedMap
 
 /**
  * Trait for a type in Type System 1 as specified in <a
- * href="https://github.com/informalsystems/apalache/blob/unstable/docs/src/adr/002adr-types.md">ADR-002</a>.
+ * href="https://github.com/informalsystems/apalache/blob/main/docs/src/adr/002adr-types.md">ADR-002</a>.
  *
  * It also contains experimental extensions that are specified in <a
- * href="https://github.com/informalsystems/apalache/blob/unstable/docs/src/adr/014adr-precise-records.md">ADR-014</a>.
+ * href="https://github.com/informalsystems/apalache/blob/main/docs/src/adr/014adr-precise-records.md">ADR-014</a>.
  */
 sealed trait TlaType1 {