diff --git a/BUILDING.md b/BUILDING.md
new file mode 100644
index 000000000..fb5feb980
--- /dev/null
+++ b/BUILDING.md
@@ -0,0 +1,104 @@
+[//]: # (SPDX-License-Identifier: CC-BY-4.0)
+
+# Building mldsa-native
+
+### Prerequisites
+
+To build **mldsa-native**, you need `make` and a C90 compiler. To use the test scripts, you need Python3 (>= 3.7).
+
+### By hand
+
+See [mldsa](mldsa).
+
+### Using `make`
+
+You can build and test **mldsa-native** as follows:
+
+```bash
+make test       # With native code backend (if available)
+make OPT=0 test # With C backend
+```
+
+To merely build test components, use the following `make` targets:
+
+```bash
+make func
+make kat
+make acvp
+```
+
+To run them, add `run_`:
+
+```bash
+make run_func
+make run_kat
+make run_acvp
+```
+
+The resulting binaries can be found in `test/build` (their full path is printed by `make`).
+
+For benchmarking, specify the cycle counting method. Currently, **mldsa-native** is supporting NO, PERF, PMU, and MAC:
+* `NO` means that no cycle counting will be used; this can be used to confirm that benchmarks compile fine.
+* `PERF` uses the `perf` kernel module for cycle counting. Does not work on Apple platforms.
+* `PMU` uses direct PMU access if available. On AArch64, this may require you to load a kernel module first, see [here](https://github.com/mupq/pqax?tab=readme-ov-file#enable-access-to-performance-counters). Does not work on Apple platforms.
+* `MAC` is `perf`-based and works on some Apple platforms, at least Apple M1.
+
+```
+# CYCLES has to be one of PERF, PMU, MAC, NO
+sudo make run_bench CYCLES=PERF
+sudo make run_bench_components CYCLES=PERF ```
+
+### Using `tests` script
+
+For convenience, you can also use the [`./scripts/tests`](scripts/tests) script as a wrapper around `make`. For
+example,
+
+```bash
+./scripts/tests func
+```
+
+will compile and run functionality tests. Similarly,
+
+```bash
+./scripts/tests bench -c PERF -r
+```
+
+will compile and run benchmarks, using PERF for cycle counting (`-c PERF`) and running as root (`-r`).
+
+For detailed information on how to use the script, please refer to
+`./scripts/tests --help`.
+
+### Windows
+
+You can also build **mldsa-native** on Windows using `nmake` and an MSVC compiler.
+
+To build and run the tests (only support functional testing for non-opt implementation for now), use the following `nmake` targets:
+```powershell
+nmke /f .\Makefile.Microsoft_nmake quickcheck
+```
+
+# Checking the proofs
+
+## CBMC
+
+### Prerequisites
+
+To run the CBMC proofs, you need specific versions of CBMC and the underlying solvers, e.g. as specified in our `nix` environment; see [nix/cbmc](nix/cbmc/).
+See [CONTRIBUTING.md](CONTRIBUTING.md) for instructions on how to setup and use `nix`.
+
+### Running the CBMC proofs
+
+Once you are in the `nix` shell or have all tools setup by hand, use `./scripts/tests cbmc` (or just `tests cbmc` in the `nix` shell) to re-check the CBMC proofs.
+See `tests cbmc --help` for details on the command line options, and [proofs/cbmc](proofs/cbmc) for more details on the CBMC proofs in general.
+
+## HOL-Light
+
+### Prerequisites
+
+To run the HOL-Light proofs, you need recent versions of HOL-Light and s2n-bignum, e.g. as specified in our `nix` environment; see [nix/s2n-bignum](nix/s2n-bignum/) and [nix/hol_light](nix/hol_light./).
+See [CONTRIBUTING.md](CONTRIBUTING.md) for instructions on how to setup and use `nix`.
+
+### Running the HOL-Light proofs
+
+Once you are in the `nix` shell or have all tools setup by hand, use `./scripts/tests hol_light` (or just `tests hol_light` in the `nix` shell) to re-check the HOL-Light proofs. Note that depending on the function, they will take a long time. See `tests hol_light --help` for details on the command line options, and [proofs/hol_light](proofs/hol_light) for more details on the HOL-Light proofs in general.
+
diff --git a/scripts/autogen b/scripts/autogen
index 0b795bc73..26ff94364 100755
--- a/scripts/autogen
+++ b/scripts/autogen
@@ -110,7 +110,7 @@ def finalize_format_batch(batch):
         if p.returncode != 0:
             print(p.stderr)
             print(
-                f"Failed to auto-format autogenerated code (clang-format return code {p.returncode}). Are you running in a nix shell? See BUILDING.md."
+                f"Failed to auto-format autogenerated code (clang-format return code {p.returncode}). Are you running in a nix shell? See CONTRIBUTING.md."
             )
             exit(1)
 
@@ -291,7 +291,7 @@ def format_content(content):
     if p.returncode != 0:
         print(p.stderr)
         print(
-            f"Failed to auto-format autogenerated code (clang-format return code {p.returncode}). Are you running in a nix shell? See BUILDING.md."
+            f"Failed to auto-format autogenerated code (clang-format return code {p.returncode}). Are you running in a nix shell? See CONTRIBUTING.md."
         )
         exit(1)
     return p.stdout
diff --git a/scripts/format b/scripts/format
index 2d801bdf0..244bfaba3 100755
--- a/scripts/format
+++ b/scripts/format
@@ -30,7 +30,7 @@ error()
 
 info "Formatting nix files"
 if ! command -v nixpkgs-fmt 2>&1 >/dev/null; then
-  error "nixpkgs-fmt not found. Are you running in a nix shell? See BUILDING.md."
+  error "nixpkgs-fmt not found. Are you running in a nix shell? See CONTRIBUTING.md."
   exit 1
 fi
 
@@ -38,21 +38,21 @@ nixpkgs-fmt "$ROOT"
 
 info "Formatting shell scripts"
 if ! command -v shfmt 2>&1 >/dev/null; then
-  error "shfmt not found. Are you running in a nix shell? See BUILDING.md."
+  error "shfmt not found. Are you running in a nix shell? See CONTRIBUTING.md."
   exit 1
 fi
 shfmt -s -w -l -i 2 -ci -fn $(shfmt -f $(git grep -l '' :/))
 
 info "Formatting python scripts"
 if ! command -v black 2>&1 >/dev/null; then
-  error "black not found. Are you running in a nix shell? See BUILDING.md."
+  error "black not found. Are you running in a nix shell? See CONTRIBUTING.md."
   exit 1
 fi
 black --include "(scripts/tests|scripts/simpasm|scripts/cfify|scripts/autogen|scripts/check-namespace|\.py$)" "$ROOT"
 
 info "Formatting c files"
 if ! command -v clang-format 2>&1 >/dev/null; then
-  error "clang-format not found. Are you running in a nix shell? See BUILDING.md."
+  error "clang-format not found. Are you running in a nix shell? See CONTRIBUTING.md."
   exit 1
 fi