Lasm：利用 Lean 4 編譯 WebAssembly，支援 Node、Serverless 與 Edge 即時部署

Lean 4 為 JavaScript 與 WebAssembly 世界而設。 Lasm 事先將普通 Lean 4 程式編譯成 WebAssembly。 一個 Lean 程式碼庫可成為 Node 伺服器、無伺服器或邊緣函式、WASI/Fastly 模組或瀏覽器應用。 因為它是 Lean，您可以證明您部署程式碼的性質。 旗艦範例，Conduit，是 RealWorld 應用，擁有 117 個已證明的定理。 Lasm 以 npm 發行，並帶入 Lean、Lake 及其建置工具；您只需要 Node（或 Bun 或 Deno）。

npm create @lasm@latest my-app -- --template hono    # then: cd my-app && npm install && npm run dev

AI 代理：此 README 本身已完整。llms.txt 是簡短索引，docs/AI.md 列出能幫您避免錯誤選項的規則。

若 Lasm 對您有幫助，我會感謝您的 贊助（詳見下文）。

快速資訊

平臺

每一行皆在 CI 中以該平臺自身的本機執行環境、映像或模擬器進行測試。\n依照專案政策，CI 永遠不會部署至真實雲端帳戶（每項測試方式）。

Node 建置包含 Lean 的完整執行環境（執行緒、檔案、程序、套接字）。\n邊緣、Bun/Deno、WASI 與瀏覽器建置則以單執行緒執行 Lean，沒有套接字或程序（檔案亦除外，僅 WASI 例外）；其餘 Lean 功能仍可使用。

從此開始

每個範例都有一個 README，提供一行指令即可執行；examples/README.md 列出全部範例。

旗艦範例：Conduit，擁有 117 個已證明的定理

examples/conduit 是 Conduit， RealWorld 應用（類似 Medium 的雜誌平臺），完全使用 Lean 撰寫：REST API、伺服器端渲染的瀏覽器應用程式以及相關證明。

• 117 個定理 關於實際執行的程式碼，已在沒有 sorry 的情況下檢查，僅使用 Lean 的標準公理 (npm run proofs；PROOFS.md) 以純英文列出每一個。它們涵蓋授權（僅作者能修改自己的文章與評論）、關注與收藏、永不衝突的 slug、永不跳脫或重複的分頁、客端與伺服器共用的驗證（應用程式永不傳送伺服器會拒絕的資料）、JSON 迴圈傳遞以及 Markdown 連結安全性。端點是針對一組 Store 函式編寫，證明則在表格模型上執行相同程式碼。
• 可信但未證明的內容：每個 SQL 語句是否按其模型執行、JSON 文本層、請求間的併發，以及 Lean、Lasm 和 JavaScript 執行環境。整個 RealWorld 規格的符合性是經測試而非證明。
• API：官方 RealWorld API 套件在 Node (node:sqlite)、Cloudflare Workers (D1) 與 Bun (bun:sqlite) 上未作任何修改即可通過（13/13 檔案，154 個請求）。每個目標都擁有一個手寫的 @[js] 繫結模組。
• 前端：Lasm.UI 執行於 RealWorld 官方模板，具備伺服器端渲染、載入與在 Lean 中解析 Markdown。官方 Playwright 端到端測試在 Node (Chromium、Firefox、WebKit) 與 Workers、Bun (Chromium) 上皆能一次通過。

所有這些在 CI 中執行（conduit.yml，執行編號 40615274657，使用 @lasm/cli 0.3.4）。

cd examples/conduit
npm install                                   # @lasm/cli, Hurl and Playwright (the official suites' runners)
npm run build && npm start                    # http://localhost:3000: the app and its API on Node
npm run proofs                                # check all 117 theorems
npm test                                      # the official API suite (also test:workers, test:bun)
npx playwright install chromium && npm run test:e2e   # the official end-to-end suite
npm run build:workers && npx wrangler dev     # Cloudflare Workers with local D1
npm run build:bun && npm run start:bun        # Bun with bun:sqlite

60 秒啟動

單一檔案不需要專案。將此完整程式儲存為 Main.lean：

def main : IO Unit := do
  IO.println s!"Hello from Lean! 2 + 3 = {2 + 3}"

npx @lasm/cli Main.lean          # builds and runs: Hello from Lean! 2 + 3 = 5
npx @lasm/cli build Main.lean    # writes dist/; run it with: node dist/main.mjs

在新機器上第一次建置會下載 Lean 與建置工具一次（約 250–275 MB；Linux CI 執行器上首次建置耗時 19 秒）。之後一次行程變更的開發建置大約 1–2 秒。

範例

每個範例皆完整：建立、開發、建置、部署。Lasm 從不安裝或啟動平臺自己的 CLI（wrangler、vercel、fastly 等）；這些由你自行執行。 npm run dev 是 lasm dev：每次儲存後約 2 秒重新建置並重啟伺服器，並在發生型別錯誤時保留上一次成功建置。

Node 伺服器（Hono；亦可使用 express、fastify、std-http、fetch）。

npm create @lasm@latest my-api -- --template hono
cd my-api && npm install
npm run dev                                   # http://localhost:3000/hello/Ada
npm run build && npm start                    # dist/ needs only Node 24+
docker build -t my-api . && docker run -p 8080:8080 my-api   # the generated Dockerfile

AWS Lambda / Vercel / Netlify / Azure / Google Cloud Functions。

npm create @lasm@latest my-fn -- --template hono --deploy lambda-zip   # or vercel, netlify, azure, gcf, lambda-edge
cd my-fn && npm install
npm run build:lambda                          # dist/ and lambda.zip (handler lasm-lambda.handler)
# deploy lambda.zip with the AWS console, aws CLI or SAM; recipes: docs/deploy/lambda.md

Cloudflare Workers（以及 Vercel Edge、Netlify Edge、Deno Deploy、Supabase）。

npm create @lasm@latest my-edge -- --template hono --deploy workers
cd my-edge && npm install
npm run build:workers                         # workers/ (wrangler.toml came from lasm init)
npx wrangler dev                              # local workerd; npx wrangler deploy to publish

Fastly Compute、WASI、Spin。

npm create @lasm@latest my-svc -- --template fetch --deploy fastly --deploy spin
cd my-svc && npm install
npm run build:fastly && fastly compute serve  # Viceroy on http://127.0.0.1:7676
npm run build:wasi-http && spin up            # or: wasmtime serve wasi-http/main.wasm

瀏覽器應用程式。

npm create @lasm@latest my-web -- --template web
cd my-web && npm install
npm run dev                                   # http://127.0.0.1:5173, live reload
npm run build                                 # dist/: a static site for any host or CDN

全端 (伺服器 + 瀏覽器 + 已驗證 API)。

npm create @lasm@latest my-app -- --template fullstack
cd my-app && npm install
npm run dev                                   # one URL: http://127.0.0.1:3000
npm run build && npm start                    # Node; also build:workers, build:bun, build:deno

編輯器。 每個專案執行一次 npx lasm editor；lasm init、lasm dev 和 lasm build 也同樣執行。Lean 編輯器 (VS Code 的 Lean 4 擴充套件) 接著解析 import Lasm.* (詳細資訊).

整個堆疊使用 Lean，已驗證

fullstack 範本是一個 Lean 專案，包含伺服器 (Lasm.Fetch)、瀏覽器應用程式 (Lasm.UI) 與它們之間的 API (Lasm.RPC)。請求必須滿足的規則在 Shared.lean 中一次性撰寫並證明，雙方皆匯入此規則 (templates/fullstack)：

-- Shared.lean
@[irreducible] def checkTitle (title : String) : Except String Unit :=
  let n := (clean title).length
  if n = 0 then .error "Write something first."
  else if n > maxTitle then .error s!"Keep it under {maxTitle} characters."
  else .ok ()

/-- Proved once, holds in the browser and on the server. -/
theorem checkTitle_ok {title : String} (h : checkTitle title = .ok ()) :
    0 < (clean title).length ∧ (clean title).length ≤ maxTitle := by
  unfold checkTitle at h
  by_cases h0 : (clean title).length = 0
  · simp [h0] at h
  · by_cases h1 : (clean title).length > maxTitle
    · simp [h0, h1] at h
    · omega

def addTodo : Endpoint NewTodo Todo := { name := "addTodo", validate := fun r => checkTitle r.title }

-- Server.lean: storing a todo demands the proof that its title passed the check,
-- and `addTodo.serve` hands the handler that proof (`ok`) after re-validating.
def Store.add (s : Store) (title : String) (_ : checkTitle title = .ok ()) : Store × Todo :=
  let t := { id := s.next, title := clean title, done := false }
  ({ todos := s.todos.push t, next := s.next + 1 }, t)

  addTodo.serve fun req ok => do
    let (s, t) := (← load kv).add req.title ok
    save kv s
    return .ok t

-- Client.lean: a theorem about the browser app: it never sends an invalid title.
theorem add_invalid (m : Model) (e : String) (h : checkTitle m.draft = .error e) :
    (update .add m).2.effects = [.msg (.added (.error (.invalid e)))] :=
  addTodo.call_invalid { title := m.draft } Msg.added "" e h

證明所在位置及其檢查方式。

未證明，改在 CI 中測試：客戶端與伺服器之間的 JSON/HTTP 傳輸、將修補程式套用至真實 DOM 的 JavaScript、Lasm 編譯器與執行時，以及瀏覽器。Lean 本身的編譯器仍被信任，與任何 Lean 程式相同 (UI.md, RPC.md)。

從 Lean 呼叫 JavaScript 與 npm

以一行宣告每個你呼叫的 JavaScript 函式；Lean 型別說明值如何轉換。完整程式 (Node 的全域 fetch)：

import Lasm.JS
open Lasm.JS

/-- `await fetch(url, init)` (Node's global fetch) -/
@[js "globalThis" "fetch"] opaque fetch : String → Data → IO Value

def main : IO Unit := do
  let response ← fetch "https://example.com" (obj [])
  IO.println s!"{← response.get "status" Nat}: {(← response.callMethodAwait "text" #[] String).length} characters"

編寫繫結的規則：

• @[js "module" "export"] opaque name : A → B → IO R 繫結 module.export。模組為 npm 套件 ("marked")、Node 內建 ("node:fs")，或 "globalThis" 用於全域。"new Hono" 呼叫構造函式，"" 為模組自身的值。
• 在 IO R 結束型別以一次性返回值，在 Async R 結束型別以回傳 promise。Async 繫結會被 await 而不佔用 Lean 執行緒。
• 使用 String、Nat、Int、Float、Bool、ByteArray、Array、List、Option、 元組、Data（任何 JS 資料）或 Value（JS 物件參考：get、callMethod、callMethodAwait）。 你自己的結構可用 deriving ToJS, FromJS 轉換。
• Function.ofFn / Function.ofFnReply 將 Lean 函式轉為 JS 回呼。 框架處理程式使用它們（見 hono、express 與 fastify 範本）。
• npm install 為位於 lakefile 旁的套件。lasm build 檢查每個繫結是否符合已安裝的套件 (Lasm.JS binding check failed: … export "x" is missing)，並將正式依賴複製至 dist/node_modules。
• 每次呼叫都從 Lean 執行緒跨到 Node 主執行緒（約 24 µs），因此 建議使用一次較大的呼叫而非多次小的呼叫。

完整指南，包含 Express、Hono、pg、jose 與 fetch 範例及代理人清單：docs/JS_BINDINGS.md。

測量數值

所有數值皆來自於免費 GitHub 執行器 (4 核 AMD EPYC, Linux x64) 的 CI，候選版本 0.1.0-experimental.40494203854 (2026-10-27)，除非另有命名。 完整表格、方法與注意事項：BENCHMARKS.md。

Lean 在 Node 上支付 WebAssembly 及其執行緒的成本。冷啟動是 CPU 限制的，因此它在小型 serverless CPU 分配上成長，每一次 JavaScript 呼叫都跨執行緒。 Pure‑Lean Std.Http 在 Node 上很慢 (1,290 req/s)，因此請使用 Hono、Express、Fastify 或 Lasm.Fetch 作為生產 HTTP。對於千位數的數字進行算術運算 比本機 Lean 更慢（沒有 GMP）。

已知限制

• 僅限預編譯。 已部署程式無法擴充、評估或編譯 Lean、載入模組資料或外掛，或在執行時使用 Lean 的 C++ 編譯器/核心 (exact list)。證明、策略、巨集與 #eval 於編譯時執行，照常。
• Lean 4.35.0 必須完全相同。 其他 lean-toolchain 版本會被拒絕，並顯示 訊息。
• Node： 為應用程式至少提供 512 MB；它會保留約 22 GB 的虛擬位址 空間。預編譯的原生函式庫（-l、共享函式庫）無法連結；套件 的捆綁 C 原始碼會為你編譯。
• Edge、Bun/Deno、瀏覽器、WASI：單執行緒 Lean；沒有 sockets、processes 或 signals；除 WASI 外沒有檔案。在瀏覽器中，阻塞等待會停止應用程式 除非它使用 --suspend jspi 為帶 JSPI 的瀏覽器構建；請使用 Async。
• 沒有預製繫結 用於 npm 套件；Lasm.Web 覆蓋核心網路平臺。
• 編輯器： Lasm.* 匯入在編輯器中於 npx lasm editor (上方) 之後解析。
• 平臺：不支援 Windows ARM64 以及 Alpine/musl 建構機器（已建構的應用程式在 Alpine 上執行）。託管平臺以其本機工具測試，從不使用真實帳戶。

檔案

• 開始： 入門 · 所有檔案 · AI 代理 · llms.txt
• 指南： 伺服器與 npm 互操作 · 無伺服器與容器 · Edge · Bun 與 Deno · 瀏覽器 與 Lasm.UI · 全端 (Lasm.RPC) · Lasm.Fetch · WASI 與 Fastly · 編輯迴圈
• 證據： 基準測試 · 應用執行位置 · 語言覆蓋 · 相容 Lean 套件 · 決策

支援 Lasm

如果 Lasm 對你有用，或你想看到它成功，我會感謝你的 贊助：github.com/sponsors/lastmjs。 它支援我和對 Lasm 以及其他 Millillion 專案的工作。我的首要目標是每月 250 美元，足以維持一個專用的 Claude Code 帳號 供 Lasm 使用。你也可以透過星標倉庫、嘗試它，並 回報什麼地方出錯。

參考

以下所有內容即為精確合約：所有指令與選項、支援的 機器與平臺，以及已部署 Lean 程式無法執行的具體事項。

CLI 參考

使用 npm install -D @lasm/cli 安裝至專案中（bin 是 lasm），或直接執行而不需安裝：npx @lasm/cli Main.lean。npm create @lasm 會執行相同 lasm init 版本的 @lasm/cli，且引數保持不變。搭配來自 快速入門 的 Main.lean：

npx lasm Main.lean                          # build (dev profile) and run: Hello from Lean! 2 + 3 = 5
npx lasm build Main.lean                    # write dist/ (release profile)
npx lasm --version                          # version, Lean, runtime and platform (for bug reports)
node dist/main.mjs                          # run the deployment: only Node is needed
npx lasm build Main.lean --target lambda    # dist/ and an AWS Lambda zip

--rebuild 與 --verbose 適用於 run 與 build。--output 與 --target 僅適用於 build；-- 之後的引數僅適用於 run。應用程式的結束狀態會被保留。npx lasm --version (-v) 會列印版本、Lean 發行版本、JavaScript 執行環境與平臺（請將其包含在錯誤回報中）。沒有 install、clean 或 uninstall 子指令。

組建設定檔 (Build profiles)。兩者都會使用相同的函式庫連結同一個程式且具備決定性。release（lasm build、lasm Main.lean --release）：完整的 Binaryen 最佳化；位元組可重現；適用於部署。dev（lasm Main.lean、lasm dev、lasm build --dev）：略過這些處理程序，並以 -O1 編譯您的模組；其行為相同，建置速度快上幾秒鐘，且其 program.wasm 大約大 15–20 %。開發重新組建會從專案先前的組建開始，因此其位元組可能取決於該組建。build-info.json 會記錄 "profile"。除非您傳入 lasm package，否則 lasm build --dev --target <platform> 與 --allow-dev 會拒絕開發組建。

環境變數（皆為選填）：

原始程式碼中的其他 LASM_* 變數是維護人員的診斷工具，並非受支援的介面。

安裝。 npm install @lasm/cli 透過您自己的 registry、proxy 與 cache，將 Lean 與建置工具以精確鎖定版本（exact-pinned）的 @lasm/… npm 套件形式提供給您的平臺。Lake/Lean-import 資料，以及僅針對含有 C 程式碼之 Lake 專案的 C 層級（@lasm/lean-c-<platform>），會在首次使用時透過您的 npm 進行抓取。 終端機會顯示進度；後續的建置會重複使用已驗證的工具與未變更的輸出。在一部沒有下載過的新機器上，首次 Hono 建置在 CI 執行器上花費了 25.7 秒（Linux x64）、27.8 秒（Linux arm64）、44.4 秒（Windows）、58.7 秒（Apple Silicon）以及 141.9 秒（Intel Mac） （建置時間，執行編號 40131930601）。 快取位置與復原：NODE_SUPPORT.md、 INSTALLATION_HARDENING.md。 僅有當 Lake 專案具有 Git 或 Reservoir 相依性時才需要 Git；Lasm 會使用您 PATH 上的 git，並在遺失時提示如何安裝。

現有的 Lake專案 可直接從專案目錄使用 npx lasm build Main.lean 進行建置。請在 lean-toolchain 中釘選 leanprover/lean4:v4.35.0；其他版本將會被 Unsupported Lean toolchain … Lasm supports Lean v4.35.0 拒絕。 各套件相容性列表 涵蓋 Batteries、Cli、LSpec、Plausible、Aesop、Qq、leansqlite、UnicodeBasic、MD4Lean、lean-zip、lean4-parser、lean-redis 與其他套件；未列在其中的套件尚未經過測試。

支援的環境

使用 Lasm（編譯器）進行建置的機器：

Node 24 或更新版本（已測試：24.0.0、24.22.1、26.12.1）。無引擎旗標。確切測試的成品：NODE_ACCEPTANCE.md。

支援的平臺

Node dist/ 需要 Node 24 或更新版本（Node 22 及更舊版本會以 This application requires Node 24.0.0 or newer 終止）以及至少 512 MB 記憶體。它可以從任何支援平臺上的建置執行於 Linux x64 與 arm64（glibc 2.28+ 或 musl/Alpine），並可在建置機器自身的平臺上執行。請複製 dist/ 的全部內容；該處不需要 Lean 原始碼、npm install 或建置工具。下方各平臺皆已在 CI 中使用指定的本地執行階段、映像檔或模擬器進行測試；均未使用真實的雲端帳戶。完整矩陣：DEPLOYMENT.md。

在 Windows 上建置並複製到 Linux（非透過 docker build）的 dist/ 需要 chmod 755 dist/host/native/process/linux-*。Node 的 --jitless 無法運作（它會停用 WebAssembly）。對虛擬記憶體設限的主機（ulimit -v、vm.overcommit_memory=2）會拒絕該 Node 建置，因為它預留了大約 22 GB 的位址空間。Node 26 的官方二進位檔在自行安裝 tarball 的極簡映像檔上需要 libatomic1。

精簡支援與限制

建置強制執行超前執行（ahead-of-time execution）。 支援一般函式、遞迴、閉包、歸納型別、模式比對、型別類別、相依型別與編譯好的 IO。匯入、巨集、精緻化（elaboration）、策略（tactics）、衍生（deriving）、證明與 #eval 會在託管的原生 Lean 中於編譯期間執行。初始設定式算作執行階段相依性：廣泛的 import Lean 可能會保留編譯器；當只有巨集或策略需要時請使用 meta import Lean，而執行階段資料庫則使用較窄的匯入（帶有 Lean.Json 的 import Lean，以及 deriving ToJson, FromJson，建置並執行）。每次拒絕都會詳細說明：Lasm 會列印從你的程式碼到編譯器程式碼的相依鏈，當廣泛匯入是原因時，則會列印你的程式碼所使用的較窄模組。部署的程式碼會如原生 Lean 一樣遵守 LEAN_ABORT_ON_NONLINEAR=1。各平臺的結果：語言涵蓋範圍。

部署的應用程式無法使用：

建置會檢查可達成的執行階段相依性，包含匯入的函式庫與間接呼叫；即使您的輸入不會執行該分支，可達成的禁止呼叫仍會遭到拒絕，且連結器移除的死碼不在此限。啟動器也會在載入應用程式之前，拒絕遺失、過時或不相容的功能記錄（這是一致性檢查，而非安全性沙箱）。這裡沒有大型相容性備援機制。

Lake 套件。僅為編譯而匯入的模組（例如戰術、展開器，例如 Aesop、Qq 或 import Lean 用於巨集）不會將 Lean 的編譯器留在部署中。Lasm 僅在程式使用其定義或註冊的東西時，或者當它們是程式執行 I/O 或呼叫 C 的自有程式碼時，才會執行模組的初始化函式（--verbose 顯示略過了多少個）。套件所綑綁的 C 原始程式碼（extern_lib、moreLinkObjs，例如 leansqlite 的 SQLite）會使用 Lean 自家的 clang 進行編譯，作為 C 層級取得一次（39–52 MB）；不需要系統 C 編譯器（macOS 需具備適用於 C 函式庫標頭檔的 Xcode Command Line Tools SDK）。無法連結預先建置的原生函式庫（共用函式庫、-l 選項：libcurl、OpenSSL、libpq、BLAS）；建置會列出函式庫與套件名稱。

非版本釋出保證。主控臺輸出、引數、結束程式碼、本機 Lake 匯入以及選定的語言/檔案系統測試具備原生與 Node 的對照測試，且在 0.1.0 之前，Lean 支援執行階段的上游套件與 19 個生態系統專案在所有五個平臺上執行，與前一個接受的候選版本相比零迴歸（0.1.0 閘道）。不保證完整的 IO.FS、並行處理、子處理序/訊號/終端機一致性、每個第三方函式庫以及完整的上游套件（I/O 差距）。大數字（超過 63 位元的 Nat/Int）使用 Lean 自家的任意精度程式碼來取代 GNU MP，因此應用程式不包含任何 LGPL 程式碼；結果與原生 Lean 相同，但在 Wasm 中，10,000 位數的乘法大約比使用 GMP 慢 5 倍，而 Nat.gcd 大約慢 60 倍（數字）。Lake 相依性會使用您的系統 Git（系統 Git）。

版本釋出與來源追溯

0.1.0 是第一個 npm 版本（注意事項）；0.2.0 新增邊緣目標與 Bun/Deno（注意事項）；0.3.0 新增瀏覽器、Lasm.UI、全端應用程式、WASI/Fastly 與編輯器支援（注意事項）；0.3.1 將入門程式碼納入 MIT-0 授權並新增錯誤回報指標（注意事項）；0.3.2 修復 Std.Internal.UV 通訊端、計時器與訊號（注意事項）；0.3.3 從未發布，其變更已在 0.3.4 中隨附（注意事項）；0.3.5 更新 README 與 Conduit 範例（注意事項）。Lasm 的 npm 套件（@lasm/cli、@lasm/create 以及 @lasm/… 工具套件）僅透過 release.yml 工作流程發布，並透過具備來源追溯功能的 npm 受信任發布機制進行：沒有任何 npm 權杖存在。版本釋出是一個會提升 package.json 版本的 Pull Request，且僅在釋出的 Commit 通過 release-checks 狀態（五平臺候選檢查；邊緣、Bun/Deno、瀏覽器、Lasm.UI、WASI/Fastly、全端、單元與開發迴圈檢查；以及確切套件的 npm 排練）後才會發布。發現錯誤？npx lasm --version 會提供錯誤回報表單要求的版本行。npm view @lasm/cli@<version> 顯示來源追溯，而專案中的 npm audit signatures 則可進行驗證。詳細資訊：RELEASING.md。

授權條款

Lasm 的原始碼採用 MIT License（版權所有為 Jordan Last）。 入門程式碼——lasm init 與 npm create @lasm 放到新專案中的所有內容、templates/、examples/ 以及本 README 和 docs/ 中的程式碼範例——在所有版本中也採用 MIT No Attribution (MIT-0)：它是你的，無需署名。@lasm/create 採用 MIT，而 @lasm/cli 的 license 欄位是 Lasm 的 MIT、MIT-0 及其捆綁的所有元件的 SPDX 表示式，其文字位於 licenses/ 中。授權審計列出了每個分發的元件、其授權以及如何滿足各項義務。

• 建置 dist/。 THIRD_PARTY_NOTICES.txt 從 Lasm 的 MIT 宣告與 Lasm 修改過的 Lean 檔案清單開始，接著是建置內容的授權：Lean 的執行環境與標準程式庫 (Apache-2.0)、Emscripten (MIT OR NCSA)、musl、LLVM libc++、libc++abi、libunwind 與 compiler-rt、mimalloc、libuv、koffi 以及 Lasm 的主機 (MIT)。應用程式不包含任何 copyleft 程式碼。licenses/<package>/ 存放編譯進 program.wasm 的所有 Lake 相依性的授權檔案；透過 npm 互通性，node_modules/ 存放各自帶有授權的每個套件。當你分發 dist/ 時，請保留這些檔案。
• Edge、瀏覽器、WASI、Fastly 與 wasi-http 輸出會獲得相同的宣告，並經重寫以說明其檔案包含的內容，且為自動產生：每個輸出目錄中的一個 THIRD_PARTY_NOTICES.txt、平臺上綑綁的 JavaScript 上的簡短 /*! … */ 授權橫幅（edge 黏合程式碼、瀏覽器載入器）、伺服器端輸出之 Wasm 內部完整的宣告檔案（一個 lasm.notices 自訂區段，因此它會隨著每次部署一起傳輸）、Fastly 套件中的檔案，以及 Vite 建置中的 THIRD_PARTY_NOTICES.lasm.txt。這對你的應用程式意味著什麼：docs/LICENSING.md。
• 工具套件與發布封存檔。 每個 @lasm/… 工具套件都有一個 SPDX license 欄位與封存檔的授權檔案。Lean 封存檔所包含的 (L)GPL 部分（GNU MP、GNU C Library、GCC 的執行環境程式庫、Linux UAPI 標頭檔、MinGW-w64）的確切原始碼以及 Lasm 自己的原始碼，都作為發布它們的發布版本的資產進行映象備份（lean-4.35.0-tiers-v2）。 Lasm 不隨附 Git 與 Apple SDK 檔案。
• Lean 名稱與標誌是 Lean FRO 的商標。Lasm 未附屬於 Lean FRO，也未得到其背書。