diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 7cbccd2..c8f2670 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -63,3 +63,30 @@ jobs:
 
       - name: Test
         run: just test-no-coverage
+
+  no_alloc:
+    name: Build / no-std, no-alloc
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+
+      - name: Install Determinate Nix
+        uses: DeterminateSystems/determinate-nix-action@d96678350ffd6a456235832eb11e1c491589b7bb # v3.21.8
+        with:
+          extra-conf: lazy-trees = true
+
+      - name: Set up FlakeHub Cache
+        uses: DeterminateSystems/flakehub-cache-action@77c6bddd7d747943530aaa578c57f233ee5d920e # v3.21.8
+
+      - name: Install Rust (stable)
+        uses: actions-rust-lang/setup-rust-toolchain@166cdcfd11aee3cb47222f9ddb555ce30ddb9659 # v1.17.0
+        with:
+          toolchain: stable
+          target: thumbv6m-none-eabi
+
+      - name: Enter Nix devshell
+        uses: nicknovitski/nix-develop@9be7cfb4b10451d3390a75dc18ad0465bed4932a # v1.2.1
+
+      - name: Build (no-std, no-alloc)
+        run: just build-no-alloc
diff --git a/.gitignore b/.gitignore
index e9b2ce0..d2cf712 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,6 @@
 # rust
 /target/
+/ensure-no-alloc/target/
 **/*.rs.bk
 
 # direnv
diff --git a/README.md b/README.md
index 5f5bbd1..16a6e66 100644
--- a/README.md
+++ b/README.md
@@ -22,6 +22,14 @@ Annotate functions and methods with "contracts", using _invariants_, _pre-condit
 
 [dbc]: https://en.wikipedia.org/wiki/Design_by_contract
 
+## `no_std` support
+
+Contracts support `#![no_std]` consumers without an allocator. No feature flag is required. The procedural macro runs on the build host and uses `std` there; the generated checks do not. Contract expressions must also be compatible with `no_std`. Logging and MIRAI modes depend on the consumer's logging or MIRAI setup and are not covered by this guarantee.
+
+CI builds the `ensure-no-alloc` consumer for `thumbv6m-none-eabi`, with `just build-no-alloc`.
+
+## Example
+
 ```rust
 pub struct Library {
     available: HashSet<String>,
diff --git a/ensure-no-alloc/Cargo.lock b/ensure-no-alloc/Cargo.lock
new file mode 100644
index 0000000..26428d3
--- /dev/null
+++ b/ensure-no-alloc/Cargo.lock
@@ -0,0 +1,54 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 3
+
+[[package]]
+name = "contracts"
+version = "0.6.9"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "ensure-no-alloc"
+version = "0.0.0"
+dependencies = [
+ "contracts",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.107"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.47"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "syn"
+version = "3.0.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "12df2e0110f65b775f769bb17ef989067a1d931b2eb822bd4346631eeada89f9"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
diff --git a/ensure-no-alloc/Cargo.toml b/ensure-no-alloc/Cargo.toml
new file mode 100644
index 0000000..1773d2c
--- /dev/null
+++ b/ensure-no-alloc/Cargo.toml
@@ -0,0 +1,7 @@
+[package]
+name = "ensure-no-alloc"
+publish = false
+edition = "2018"
+
+[dependencies]
+contracts = { path = ".." }
diff --git a/ensure-no-alloc/src/compat_test.rs b/ensure-no-alloc/src/compat_test.rs
new file mode 100644
index 0000000..9e1aa6d
--- /dev/null
+++ b/ensure-no-alloc/src/compat_test.rs
@@ -0,0 +1,46 @@
+use contracts::*;
+
+#[contract(
+    requires(value < u32::MAX, "Increment must not overflow"),
+    ensures(ret == value + 1),
+)]
+fn increment(value: u32) -> u32 {
+    value + 1
+}
+
+struct Counter(u32);
+
+#[invariant(self.0 < 100)]
+impl Counter {
+    #[debug_requires(self.0 < 99)]
+    #[debug_ensures(self.0 == old(self.0) + 1)]
+    fn increment(&mut self) {
+        self.0 = increment(self.0);
+    }
+}
+
+#[contract_trait]
+trait ReadCounter {
+    #[ensures(ret < 100)]
+    fn read(&self) -> u32;
+}
+
+#[contract_trait]
+impl ReadCounter for Counter {
+    fn read(&self) -> u32 {
+        self.0
+    }
+}
+
+#[test_requires(value < 100)]
+#[test_ensures(ret == value)]
+#[test_invariant(value < 100)]
+fn identity(value: u32) -> u32 {
+    value
+}
+
+pub fn exercise() {
+    let mut counter = Counter(0);
+    counter.increment();
+    assert_eq!(identity(counter.read()), 1);
+}
diff --git a/ensure-no-alloc/src/main.rs b/ensure-no-alloc/src/main.rs
new file mode 100644
index 0000000..64faea0
--- /dev/null
+++ b/ensure-no-alloc/src/main.rs
@@ -0,0 +1,21 @@
+#![no_std]
+#![no_main]
+
+// Do not add a global allocator: the build must fail if generated contracts require one.
+mod compat_test;
+
+#[panic_handler]
+fn panic(_info: &core::panic::PanicInfo<'_>) -> ! {
+    loop {
+        core::hint::spin_loop();
+    }
+}
+
+#[no_mangle]
+pub extern "C" fn _start() -> ! {
+    compat_test::exercise();
+
+    loop {
+        core::hint::spin_loop();
+    }
+}
diff --git a/justfile b/justfile
index b6592ac..184097d 100644
--- a/justfile
+++ b/justfile
@@ -43,10 +43,16 @@ test-no-coverage:
     RUSTDOCFLAGS="-D warnings" cargo {{ toolchain }} doc --workspace --no-deps --all-features
 
 # Test workspace and generate coverage files
-test: test-no-coverage
+test: test-no-coverage build-no-alloc
     # @just test-coverage-codecov
     # @just test-coverage-lcov
 
+# Build a consumer without the standard library or an allocator.
+build-no-alloc:
+    cargo {{ toolchain }} build --target=thumbv6m-none-eabi --manifest-path=ensure-no-alloc/Cargo.toml
+    # Compile test-only contracts without the standard test harness.
+    cargo {{ toolchain }} rustc --target=thumbv6m-none-eabi --manifest-path=ensure-no-alloc/Cargo.toml -- --cfg test
+
 # Test workspace using MSRV
 test-msrv: downgrade-for-msrv test
 
diff --git a/src/lib.rs b/src/lib.rs
index c2622e3..879675d 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -17,6 +17,14 @@
 //! If the last argument to an attribute is a string constant it will be
 //! inserted into the assertion message.
 //!
+//! ## `no_std` support
+//!
+//! Contracts support `#![no_std]` consumers without an allocator. No feature flag is required.
+//! The procedural macro runs on the build host and uses `std` there; the generated checks do not.
+//! Contract expressions must also be compatible with `no_std`.
+//! Logging and MIRAI modes depend on the consumer's logging or MIRAI setup and are not covered
+//! by this guarantee.
+//!
 //! ## Example
 //!
 //! ```rust