Velaris

适用对象。 即将运行模型编写的程序的人——无论是在笔记本电脑上、 CI 中，还是 MCP 服务背后——他们希望程序可访问的内容受自己声明的权限 限制，而不是取决于程序如何描述自身。它限制的是用 Sabline 编写的程序， 而非同一个模型可能会改用 Python 或 shell 编写的脚本。

一条命令，看它如何拒绝——无需参数、不访问网络，不到一分钟。它会 编写一类 Agent 常写的脚本（读取 ./.env，并将其发送到 webhook）， 在未授予任何预算的情况下运行脚本，展示拒绝结果和运行回执；随后在 预算范围内执行相同任务：

pip install sabline-lang
sabline demo

error[E310] 'read_file' needs the 'fs' effect, which this run does not allow (it allows: io)
exit 1. receipt: refused; E310 (fs) at line 6; grants used: none
3 setting(s); the report is in out/report.txt

它只写入自己运行的内容，不读取你的任何文件；--keep 会保留文件， 而 sabline receipt show 会将任一回执渲染为页面。

---

本项目在 8.6.0 之前名为 Velaris。 该名称与同一市场中的一家无关 公司（velaris.io）重名，因此项目选择放弃，而非争夺。除此之外一切 不变，并且在 8.x 中，针对旧名称编写的所有内容仍可正常工作：velaris 命令、import velaris、VELARIS_* 环境变量、已提交的 velaris.capabilities，以及 velaris.audit/1 或 velaris.receipt/1 文档都会继续读取，并且每项都会说明一次名称已更改。 docs/renamed.md 列出了所有已发布地址及其现在的指向； STABILITY.md 说明了 9.0 中的内容。

---

pip install sabline-lang
sabline agent_output.vel

该程序无法打开套接字、读取文件、调用 Python，也无法读取时钟。这不是 “最好不要这样做”——运行时会直接拒绝，而且无法捕获拒绝结果并绕过它。 你不必阅读代码、理解代码，也不必相信编译器对代码的分析。

从 5.0 开始，不带 --allow 的运行会获得 io，即控制台权限。 过去默认会获得全部七种效果，这意味着在操作员另行规定之前，对“这个程序 可以做什么？”的回答是“一切”。通过指定程序所需权限来扩大范围 （--allow io,fs:read:./data）；--allow all 会授予所有效果，并向 stderr 写入一行说明。 --allow io,ffi:math,json 仅允许 Python 使用这些模块；任何调用若触及其他模块——无论是直接命名，还是通过已授权模块的属性触及——都会被拒绝（E311）。已授权模块仍可执行该模块自身能够执行的任何操作：ffi:os 就是操作系统。自 3.0 起，同一语法还能细化每种宽泛权限：fs:read:./data、fs:write:./out、net:api.example.com:443、net:*.example.com，以及用于限制一次运行中操作次数的 @100；env 是独立权限，因此仅有 io 权限的程序无法读取环境变量。库和每个入口都支持 timeout 和 max_memory_mb；在入口中，操作者设置的限制是调用方无法提高的上限。 这仍不是安全边界——但每次审查都提出的那些注意事项、ffi 的悬崖、无界执行，以及没有路径或主机列表的 fs 和 net，如今都成了明确的权限，而不是漏洞。对于如今所有人都面临的情况——运行由其他人或其他事物编写的程序——这是一道真正的防护。

另一半：承诺，已获证明

fn discount(price: Int) -> Int
    requires price >= 0
    ensures result >= 0
{
    return price - 10
}

error[E700] promise cannot be kept: 'discount' ensures result >= 0 - proven without running the program: price = 5 gives result = -5

这个 ensures 不是注释，也不是运行时断言。Z3 定理证明器会在执行前验证它对所有可能的输入都成立——如果它不成立，还会用精确的反例将其驳斥。

客户编写的规则

一个电商平台允许每位客户编写自己的折扣规则。这个规则具备大多数规则都有的形式：购物篮达到门槛后按百分比打折，同时再减去一笔固定金额，并为两项折扣之和设置上限。

record Rule {
    percent: Int         // this much off, once the basket is
    above: Money of INR  // worth at least this,
    flat: Money of INR   // and this much off as well,
    cap: Money of INR    // but never more than this, all together
}

fn discount_for(total: Money of INR, rule: Rule) -> Money of INR
    requires total >= money(0, "INR")
    requires rule.percent >= 0
    requires rule.percent <= 100
    requires rule.flat >= money(0, "INR")
    requires rule.cap >= money(0, "INR")
    ensures result >= money(0, "INR")
    ensures total - result >= money(0, "INR")
{
    let off = money(0, "INR")
    if total >= rule.above {
        off = percent_of(total, rule.percent, 100, "half_up")
    }
    off = off + rule.flat
    if off > rule.cap {
        off = rule.cap
    }
    if off > total {
        off = total
    }
    return off
}

这两个 ensures 让平台能够确认一条并非由它编写的规则：折扣绝不会变成附加费，折后金额也绝不会为负。对于类型所允许的每个购物篮和每条规则，这两点都能在程序运行前得到验证。 examples/discount.vel 是完整程序——其中 5 个函数全部作出了已获证明的承诺，并且程序可在 --allow io 下运行。

examples/discount_bad.vel 是删除了最后一个 if 的同一条规则。上限仍会将折扣限制在固定额度内，但没有任何条件保证折扣不超过购物篮的价值：

$ sabline check examples/discount_bad.vel
examples/discount_bad.vel:54: [E700] promise cannot be kept: 'discount_for' ensures total - result >= money(0, "INR") - proven without running the program: rule = Rule(percent: 0, above: 0, flat: 2, cap: 1), total = 0 gives result = 1

金额单位是派沙：价值为零的购物篮，固定折扣为 2 派沙、但被限制为 1 派沙，却仍然返还了 1 派沙。程序不会运行。

沙箱回答的是另一个问题。它可以阻止这条规则读取文件或打开套接字，却无法判断算术是否成立。

它无法打印的密钥

效果会说明程序打印了某些内容，但不会说明打印的内容是否为机密。Secret of T（6.0、7.0）是另一半：编译器会跟踪该值，并拒绝任何将它交给会产生输出的对象的程序。

fn key() -> Secret of Text uses env {
    return env("API_KEY", "")          // env() gives a Secret of Text
}

fn authorization(k: Secret of Text) -> Secret of Text {
    return "Bearer " + k               // still a Secret of Text
}

examples/secret.vel 会读取一个 API 密钥，构建携带该密钥的请求，并打印该请求的摘要。 examples/secret_bad.vel 是同一个程序，只多了一行：

$ sabline examples/secret_bad.vel --allow env,io
error[E560] argument 1 of 'print' is Secret of Text, and 'print' performs io - a Secret cannot be printed, written, sent or passed to Python. It came from env(), line 27, through 'key', which returns Secret of Text (line 58)
  --> examples/secret_bad.vel, line 58

没有任何内容运行，没有任何内容被记录，也不需要审核者注意到这一行。密钥列表、密钥映射，或含有一个密钥字段的记录也会携带该密钥，因此整个结构都会在输出点被拒绝——持有密钥的 Request 记录也无法打印。

程序也不能查看密钥。 key == "" 的结果是 Secret of Bool，而不是 Bool，在它上面使用 if 或 while 会触发 E563。这条规则让其余部分才有意义：结合 length 和 code_at，由 == 得到的普通 Bool 并非只有一位信息，而是一个能读出整个密钥的循环——

while at < 3 {
    for c in alphabet {
        if code_at(key, at) == code_at(c, 0) {   // E563
            found = found + c
        }
    }
    at = at + 1
}
print("recovered: " + found)                     // the whole key

——因此，如果规则禁止 print(key)，却允许这种做法，那就只是装饰，而不是类型规则。界限设在分支处。

declassify(value, "why") 是唯一的脱密途径。它要求签名中包含 uses declassify，调用时写明理由，并且运行时具有 declassify 授权——审计报告也会记录这项操作，因此使用者无需运行程序，就能询问程序是否曾让机密泄露：

$ sabline audit examples/secret.vel --json | jq .secrets
{
  "sources": ["env"],
  "declassifies": false,
  "declassifications": []
}

要查看机密，程序必须明说——declassify(key == "", "…") 会返回可用于分支判断的 Bool，代价是需要相应效果、授权，并在审计记录中写明理由。这就是取舍：不是保持沉默，而是明确声明。

这并不意味着：它只能识别由 env() 和 read_file_secret() 生成的值，因此通过 read_line 读取的密码、通过 args() 传入的密码，或通过 net 从保管库获取的密码，都只是没有任何保护的普通 Text。它也不保证无干扰——程序仍然可以选择运行多久以及是否停止。SPEC.md §3.1 说明了相关规则，THREAT_MODEL.md 说明了限制。

相关工作

TACIT（“Securing Agents With Tracked Capabilities”，ACM CAIS '26； arXiv 2603.00991）让 Agent 编写 Scala 3，其捕获检查会在类型系统中将文件、网络和命令能力作为值进行跟踪； CaMeL让模型将用户请求转化为受限的 Python 子集，并为每个值标记其来源和允许读取者，在每次工具调用时检查策略； WASI只向 WebAssembly 模块提供宿主交给它的资源。Sabline 是一种小型语言，模型可以通过一张约 5,300 个单词的卡片学会使用它；函数在其中声明自身的效果，运行时在每次操作时强制执行操作员设定的预算，合约则由 Z3 定理证明器检查。从 6.0 版起，它还会跟踪一种数据：Secret of T。env() 和 read_file_secret() 会生成这种数据；它不能流向任何会输出内容的地方，不能用于分支判断，并且只能通过 declassify 离开——这是一种独立的效果。这比 CaMeL 和 TACIT 的能力范围更窄：它们会为每个值标记来源和允许读取者，而 TACIT 还会跟踪能力在多态中的流转；Sabline 则标记两个内置函数的返回值，并会拒绝针对这些值的泛型代码，除非签名明确允许。 5.0 版之前，如果未提供预算，其命令行也会授予所有效果；而 WASI 模块在未获得任何资源时则无法触及任何资源。从 5.0 版起，不设预算的运行仅获得 io。 能力格式以 CC0 许可单独发布于 sabline-spec；其中的 PRIOR_ART.md 详细说明了这些差异及更早期的相关工作。从 4.1 版起，它还包含一套一致性测试语料库，任何语言的实现都可运行——共 456 个 JSON 用例，分为声明、强制执行和棘轮机制三个级别，均不需要定理证明器。这些用例根据本仓库的测试套件编写，并通过漂移测试确保与其保持一致；sabline conformance 会针对此实现运行测试，CI 也会在每个测试任务中运行它。

为什么选择 Sabline

保证	含义
效果清晰可见	uses io, net, fs, ffi——未声明 uses net 的函数绝不会直接或间接访问网络，未声明 uses ffi 的函数绝不会调用 Python。隐藏行为无法通过编译。
承诺经过证明	requires / ensures / 循环 invariant，由 Z3 通过模块化调用摘要进行验证——包括记录、映射、嵌套列表、带量词的列表属性、失败路径，以及真正的 IEEE-754 浮点数（证明器会用导致结果不相等的确切双精度值反驳 x + 0.1 + 0.1 == x + 0.2）。
失败不可忽略	在签名中声明 -> Int or fail；调用者必须使用 check 或 try。遗漏错误处理路径会导致编译错误，内置函数也不例外。
机密既不能打印，也不能查看	Secret of T——env() 和 read_file_secret() 的返回类型。任何会产生输出或可能失败的操作都不能接收机密；包含机密的结构会携带机密；对机密执行的每种操作都会保留其机密性（包括比较），也不能用机密作为 if 分支条件。declassify(value, "why") 是唯一的脱密方式：它本身会产生一项效果，并会在审计记录中注明原因。SPEC.md §3.1 说明了它仍未做出的保证。
在安全的情况下保持快速	对数字的纯函数、列表读取和文本操作（包括在这些函数中构建的文本）会通过 LLVM JIT 编译为本机代码（热点算术约快 10,000×，文本构建约快 45×），并通过与解释器的差分测试。本机读取会进行边界保护，文本则构建在运行时拥有的缓冲区中，因此结果始终与解释执行一致。

关于为什么浮点数按 IEEE-754 而非实数进行证明，以及这会带来什么代价，请参阅：docs/floats.md。

对于无需编写不变量也能处理的循环，编译器会自动处理那些只需简单不变量的情况：它会为每个计数器推导边界，并保留不会被循环步骤破坏的边界（参见 examples/inferred.vel）。更复杂的属性——如成员关系、有序性——仍需编写 invariant 行。

除非反例包含完整前提，否则证明器绝不会声称“无需运行即可证明”——无法转换的假设会导致证明转交运行时检查，而不是冒误报的风险。健全性报告会按安全问题处理。

安装

pip install sabline-lang
sabline doctor
sabline new hello && cd hello && sabline main.vel

独立可执行文件（无需 Python）——从最新版本下载适用于 Windows / Linux / macOS 的文件，然后：

sabline doctor

Python 3.10 及更高版本：

pip install sabline-lang
sabline new hello && cd hello && sabline main.vel

零安装——在线体验区会在浏览器中运行真正的编译器。

从源码安装时可选的附加组件：pip install ".[full]" 会添加 z3-solver（编译时证明）和 llvmlite（本机加速）；未安装这些组件时，承诺会在运行时检查，所有内容都以解释方式运行——语言相同，只是性能会相应降低。安装 llvmlite 后，默认使用本机代码：编译器能够编译的纯函数都会以机器码运行，除非使用 --no-native 强制交由解释器执行。没有 --native 标志。

日常使用体验

keep_if(xs, fn(n: Int) -> Bool { return n % 2 == 0 })   // inline functions
format("hi {}, {} left", name, count)                    // text with holes
args()                                                   // command line
post(url, body) / fetch_status(url)                      // not just GET

函数值会提升为真正的函数，因此证明和本机编译同样适用——它们也可以携带自己的 requires / ensures，并像其他函数的承诺一样接受证明。创建函数值时，会将周围的局部变量复制一份供其使用（SPEC.md §12a）；对此类函数值声明的承诺会在运行时检查。

集成位置

sabline script.vel                    the command (io unless you say more)
sabline script.vel --receipt r.json   and a signable record of what that run did
sabline eject script.vel              a directory that runs with nothing from here
import sabline                        a Python library
sabline mcp-install                   tools inside your assistant
sabline.mcpb                          double-click install for Claude Desktop
uses: gowrishankar-infra/sabline-lang a GitHub Action, findings in the Security tab
sabline capabilities check            CI fails when the capability surface widens
sabline serve                         an HTTP door for any language, token required
npx sabline-lang script.vel           npm, for the JavaScript world
%%sabline --audit --allow io          a Jupyter cell
- repo: sabline-lang (pre-commit)     a commit hook
docker run ... sabline check          a container
sabline build --for-everyone          standalone executables

在自己的程序中使用

import sabline

report = sabline.audit(source)      # what it touches, what's proven
run = sabline.run(source, allow={"io"})   # it cannot touch anything else
print(run.output, run.refused_effect)

预算的执行方式与命令行相同。此外还有一个 MCP 服务，因此助手无需离开对话，就能编写、审计并在沙箱中运行 Sabline——请参阅 EMBEDDING.md 和带版本号的 sabline.audit/1 格式。

每次使用超时或内存上限调用 run，都会启动一个全新的解释器。池可以在固定预算下让工作进程保持运行：

pool = sabline.Pool(size=4, allow={"io"}, timeout=30, max_memory_mb=512)
result = pool.run(source)             # the same RunResult run() returns
pool.close()

对一个小程序进行 200 次连续的限额运行：逐次启动进程需要 46.6 s，使用池则需要 0.5 s。pool.run 不接受 allow——预算归池所有；除非运行干净结束，否则工作进程会被终止并替换；复用的工作进程会先重置所有可变状态。check_pool.py 会验证上述每一项，包括一个通过 ffi 扩大自身预算、却无法为下一个程序扩大预算的程序。完整规则见 EMBEDDING.md。

让客户编写规则的平台

examples/platform/ 将这种模式实现为一个小型 FastAPI 服务，全部代码位于一个文件中。客户提交 Sabline 源码；服务会审计源码，连同其能力范围一起存储，并返回它声明的内容——效果、主机、路径、模块、已证明的占比、逐个函数的契约，以及能够运行它的最小预算。服务不会运行源码。如果其能力范围超出平台许可范围，服务会拒绝请求，并指出需要添加哪些授权。实际运行由预算与平台相同的 sabline.Pool 负责。

提交 examples/discount.vel，响应会显示 "proven_share": 100.0，且每项承诺的 "status": "proven"，包括对收款方最重要的两项：折扣绝不会变成附加费，剩余金额也绝不会为负数。这是平台在允许客户启用规则前可以展示给他们的说明，而沙箱无法给出这样的说明。

调用你工具的程序

sabline run agent.vel --tools tools.json \
    --allow io,tool:search@20,tool:send_email:to=*@corp.com

运行器的首个版本（8.5）。主机进程通过清单向程序提供工具——清单为每个工具定义 JSON Schema 参数、成本和上限——而运营方的预算则规定哪些工具可以调用，并将参数限制在指定模式内。任何超出这两者之一的调用都会在主机得知之前被拒绝；收据会记录每次调用、通过的模式以及上限。examples/runner/host.py 是一个完整的 Python 主机：它提供 search 和 send_email，第二个示例程序试图向 corp.com 之外的地址发送邮件时会被拒绝。协议使用标准输入和输出上的 JSON 行（docs/runner.md）；目前还没有框架适配器，工具结果也尚未标记为主机而非程序所提供的内容——这就是 9.0 中的 Untrusted。sabline skill verify 会报告技能中的程序所需的工具和预算，而不会运行这些程序。

由模型编写，由你审查，在隔离环境中运行

sabline card > card.md          # ~5,300 words: paste into any model
sabline audit script.vel        # what it can touch, before you run it
sabline attest script.vel --output script.intoto.json   # the same, bound to its bytes
sabline script.vel              # io, and nothing else, unless you say more

sabline audit 是为审查者编写的：程序会触及什么、承诺了什么、其中有多少是证明出来的，而非运行时检查的、可能出现什么故障，以及安全运行程序的确切命令。sabline attest（4.2）会将这份审计写入一个 in-toto Statement，其中的主体是程序文件及其 sha256 值，可用 cosign 或 sigstore-python 签名；EMBEDDING.md 展示了这两种方式，每个版本都会附带一份针对示例程序的签名审计。 agent_loop.py 完成了整个闭环——模型编写程序，sabline check --json 返回带修复建议的错误，然后模型不断迭代，直至程序编译通过，且其承诺得到证明。

从 8.3 开始，涵盖一次运行其余生命周期的功能：sabline eval 像评估框架一样运行程序，并采用其命令行无法放宽的配置文件（禁用网络、ffi 和 env，限制时间与内存、响应停止请求、在操作系统提供支持时隔离工作进程，并始终生成回执——见 docs/eval.md）；sabline receipts diff 会指出运行中有哪些内容不在审计或此前的运行中；sabline replay 会根据回执，用相同的字节再次运行，或拒绝运行；sabline test --from-contracts 会针对证明器认定其 requires 允许的输入，逐项测试每个承诺；sabline verify 会检查证明文件或回执是否符合其类型及字节内容。docs/structurally-impossible.md 列出了 Sabline 程序中不可能发生的情况，每项都附有测试；docs/crosswalk.md 则将每项保障和已知缺口对应到 OWASP、AIUC-1 和 NIST 框架。

运行你没有编写的代码

sabline agent_output.vel                 # io: it may print, nothing else
sabline agent_output.vel --allow io,fs:read:./data   # and read that folder
sabline agent_output.vel --allow all --deny net,ffi  # everything but these

无论源代码声称什么，运行时都会拒绝超出你授权预算的任何影响——而拒绝无法被捕获后带过。从 8.4 开始，系统还会被要求执行相同的预算，因此 Sabline 本身的故障也会被内核拦截：Linux 上使用 Landlock 和 seccomp（完整支持），macOS 上使用沙盒配置文件，Windows 上使用降低权限的令牌和作业对象（后两者均为部分支持）。sabline doctor 会说明你的机器支持哪些功能，回执会说明一次运行获得了什么，而 --no-confine 可以关闭隔离（见 docs/confinement.md）。 这不是安全边界（ffi 会授予 Python 所能执行的一切操作，并扩大系统被要求限制的范围），但确实能为运行你尚未审阅的程序提供防护。

一次性检查所有内容

sabline examples/stress.vel --allow clock,env,ffi:datetime,math,sqlite3,io,net:raw.githubusercontent.com
                                # 33 checks across the whole language
sabline examples/edges.vel --allow ffi:datetime,io
                                # 20 boundary, property and round-trip checks
python check_refusals.py        # 25 wrong programs, each refused correctly
python check_sandbox.py         # 39 escape attempts, each refused with its code
python check_confine.py         # the operating system holds the budget too (8.4)
python check_secret.py          # a Secret reaches nothing that emits it
python check_pool.py            # a pool must leak nothing between programs
python check_platform.py        # the reference platform refuses what it says it does
python check_ratchet.py         # every widening fails, nothing else does
sabline conformance             # sabline-spec's 456-case corpus, L1 to L3

一条命令即可测试语言、标准库、证明器、原生编译、JSON、日期、CSV、宿主语言和网络。

与其他工具的对比

102 个小程序——其中 80 个各有一个刻意设置的缺陷， 22 个正确对照项—— 每个都以相同行为分别用 Sabline、Deno 的 JavaScript 和 Python 编写。一个测试框架会让每个程序通过 每种工具运行，并记录运行前发现了什么、运行时发现了什么，以及 遗漏了什么。第十二类（7.1）是间接权限：调用代码在前后完全相同， 只有依赖项声明的预算在两个版本之间扩大了。

	运行前发现	运行时发现	遗漏	22 个对照项中的误报
Sabline 8.8	54	16	10	3
Deno 2.9	8	43	29	0
Python 3.13	0	32	48	0

Sabline 的十个遗漏是刻意保留在表中的。其中两个从一开始就存在：一个循环提前停止一项，但没有契约与之矛盾；一个程序为调用方打印 rm -rf build，却什么都没动。另有五类中的八个遗漏，是在 8.7 中加入、专门让 Sabline 漏掉的：将私有文件发到任务获准访问的唯一主机、 在任务所需程序旁运行第二个程序，以及获准使用的库自行进行 I/O。它的三个误报 也是刻意保留的：一个正确的循环，其终止规则无法证明它会结束——欧几里得算法 会结束，因为一个量不断减小；另外两个正确结果大到无法用 64 位整数表示。第四个 误报，即输入结束时循环也结束的情况，从 9.0 起会在主分支上报告为受输入长度限制。 每一行都列在 benchmark/RESULTS.md 中——可通过一条命令重新生成：python benchmark/run.py。同一批程序针对 WASI、 Starlark、Python 沙箱和 CaMeL 的结果也在 /competitors.html 中——它们各自在某些程序上都比 Sabline 表现更好，页面会先指出是哪一个。

值得运行的程序

examples/ledger.vel——一个费用追踪器：记录、整数分值、 文件持久化、排序报告。 examples/wordcount.vel——文本分析： sabline examples/wordcount.vel --allow fs:read,io <file> [n] 统计 词频并打印排序后的直方图。 examples/linkcheck.vel——一个真正实用的链接检查器： sabline examples/linkcheck.vel --allow io,net <url> ...，发现损坏链接时 以非零状态退出。 examples/fetcher.vel——一个 HTTP 工具：检查状态，然后概述 页面；每次网络调用都已声明，每种失败情况都已处理。

JSON

json_get(doc, "user.name")    json_int(doc, "user.age")
json_len(doc, "tags")         json_of(Person(name: "gowri", age: 30))

路径会遍历对象和列表，每次读取都可能失败（字段缺失是 一种可能，而不是崩溃），这些操作都不是副作用——解析文本 是纯操作。

调用其他语言

fn today() -> Text uses ffi or fail {
    let nothing: List of Text = []
    return try py("datetime.date", "today", nothing)
}

py / py_int / py_float / py_json 调用 Python 函数，而 py_new / py_do / py_field / py_close 持有真实对象——例如 数据库连接、会话——因此可以访问 Python 提供的所有库—— 但只能在声明了 uses ffi 的函数中使用，而且它可能像任何离开程序的操作一样失败。

标准库也能访问外部服务

import "http.vel" as http     import "db.vel" as db
import "time.vel" as time     import "env_tools.vel" as sys

check http.get(url) { ok body { ... } fail why { ... } }
check db.count(conn, "notes") { ok n { ... } fail why { ... } }

它们用 Sabline 编写，因此会携带自身的效果——使用 http 的程序会显示 net，使用 db 的程序会显示 ffi，而纯函数 两者都不能调用。

从 8.5 开始，其中四个库可以与运维脚本会访问的服务通信， 且都不调用 Python，因此使用其中一个库的程序在审计中完全不会显示 ffi：

库	访问范围	示例
azure.vel	Azure Resource Manager：GET、PUT、PATCH、DELETE、分页和 ARM 的错误。net:management.azure.com:443	azure_groups.vel：资源组和标签漂移
github.vel	GitHub REST API：仓库、问题、拉取请求、检查、发布、内容和速率限制。net:api.github.com:443	github_issues.vel
k8s.vel	Kubernetes API：list、get、watch-once；所有会更改集群的函数都以 write_ 开头	k8s_pods.vel：未处于运行状态的 Pod
aws.vel	S3 和 STS，使用 Sabline 中的 Signature Version 4 签名	aws_buckets.vel

令牌或密钥以 Secret of Text 的形式传入，库会在审计中说明它离开的唯一位置：通过 declassify 传出的 bearer 令牌，理由中会注明主机；通过 hmac_sha256_chain 传出的 AWS 签名，会标记为 hmac signature——密钥本身始终是 Secret （THREAT_MODEL.md 说明了为何这样做是安全的）。 check_batteries.py 会在每个 CI 执行环境中，针对每个库运行测试，并使用相应服务的替身。sabline-kit 是一个从 Azure 脚本开始的模板仓库。

库

sabline add https://example.com/geo.vel as geo   # vendored into lib/
sabline deps                                     # what you depend on
sabline deps --verify                            # unchanged since?

库通过编译后才会被接受，并保存在你的 仓库中，供你阅读。没有注册表，没有依赖解析器，也不会在构建时获取任何内容。

sabline add 会在 sabline.toml 旁写入 sabline.lock：记录每个供应商库及其来源、收到的确切字节的 sha256，以及添加该库时所用的 Sabline 版本。sabline deps --verify 会在文件的哈希与锁文件不符，或锁定的库不在磁盘上时失败——这条命令值得加入 CI。若要添加已供应商化但字节不同的库，操作会被拒绝并打印两个摘要；--force 会替换它。

导入

import "lib/geo.vel" as geo      // named: geo.distance(a, b)
import "std.vel"                 // flat: sort(xs)

具名导入会为该库的函数添加前缀，因此，即使两个库都导出 distance，也能在同一个文件中使用。发送到 HTTP 入口或 MCP 服务的程序，只能导入入口所服务目录内的 .vel 文件；库在指定 import_root= 时也遵循同样的规则；任何其他导入都会在读取文件之前被拒绝（E515）（8.1）。

发布程序

sabline build myprogram.vel      # one executable, ~90 MB
./myprogram alpha beta           # runs anywhere, nothing installed;
                                 # it takes --allow like the compiler

sabline build myprogram.vel --for-everyone   # a workflow that builds
                                             # Windows, Linux and macOS

将你的程序、导入项、标准库和编译器打包到一个文件中。该文件会在构建前完成编译和证明检查。

sabline eject myprogram.vel      # a directory that runs with nothing
python -I myprogram-ejected/main.py   # installed from this project

sabline eject（8.1）会将程序、导入项和一份运行时副本写入目录；其中的 main.py 会固定预算、检查每个文件的摘要，并拒绝可能让一次运行改写下一次运行的预算。目录还包含固定版本的 requirements.txt、PyInstaller 命令和 README，说明导出后仍有效的内容——预算——以及不再有效的内容：证明只是导出时的记录，之后的任何修复都不会影响它。

工具

sabline trace program.vel（实时查看每次调用）· sabline test program.vel（运行 Sabline 中编写的每个 test_* 函数）· sabline check program.vel（编译但不运行；可一次处理多个文件，工具可使用 --json）· sabline explain program.vel（逐步讲解每个函数：效果、承诺及其是否已证明 — explain <folder> 可映射整个项目）· sabline repl（定义会在输入时进行证明检查）· sabline fmt（规范格式，CI 可使用 --check）· sabline lsp （在任何 LSP 编辑器中实时显示错误；VS Code 扩展位于 editor/vscode）· sabline doctor · sabline new · 自动化可使用 --json 错误输出。

标准库

使用 Sabline 编写，位于 stdlib/std.vel — 它 也会兑现自己的承诺：sort 带有 ensures is_sorted(result)， max_of 要求列表非空，而违反库的 requires 会在你的调用处导致编译错误。完整 参考文档， 由真实编译器生成。

数字

整数为 64 位。超出该范围的算术运算会报错，而不是静默溢出 — 无论代码是解释执行还是作为机器码运行，都会报相同的错误。浮点数是 IEEE-754 双精度数，并会据此进行证明。

金额不属于这两种类型。 money(1250, "INR") 表示 12.50 卢比，以 1250 派萨存储：以次级货币单位表示的精确整数，货币单位包含在其类型中， 因此 INR 与 USD 相遇会导致编译错误，且不会让 Float 参与其中。 对金额进行除法时必须说明如何舍入 — percent_of(claim, 25, 1000, "half_up") — 否则无法编译；而 money.split(payout, 3) 会将金额拆分为若干部分，且可证明它们的总和等于 payout。请参阅 examples/settlement.vel 和 SPEC.md §4.3。

参考文档

SPEC.md 精确说明了这门语言的含义：语义、 求值顺序、效果传播、目前“已证明”涵盖的内容，以及 Sabline 刻意不具备的功能 — 包括为何它没有并发模型。

稳定性

语义化版本控制：仅在主版本中进行破坏性更改。 STABILITY.md 说明了其涵盖的内容 — 语言、 错误代码、sabline.audit/1、库 API、预算语法和 命令行 — 以及未涵盖的内容、弃用和移除规则，还有本项目每次违反该规则的情况， 包括 3.3 和 3.4。CI 会在 Linux、Windows 和 macOS 上， 使用 Python 3.10 和 3.12，并分别在安装和未安装可选依赖项的情况下测试每次推送。错误代码 保持稳定且带有编号，并且 有完整文档。

有多少内容已得到证明

sabline proofs .            # how many promises are proven, file by file
sabline proofs . --min 80   # fails the build below 80%

对于此代码库中的示例和标准库，sabline proofs examples stdlib 会在函数运行前证明 99 个作出承诺的函数中，有 70 个函数的承诺， 已证明比例为 70.7%；其余函数会在运行时进行检查。其中有些 示例专门设计为无法通过检查，其承诺本来就是错误的。

在 CI 中使用 Sabline

GitHub Action 会审计仓库中的 Sabline 程序（即 .vel 文件），并将它们可能触及的内容报告到 GitHub 代码扫描中。 它不会读取 Python、JavaScript、Go 或其他任何内容：没有 .vel 文件的仓库会打印 no .vel files found，且作业会成功。 它所服务的场景很具体，这也是这门语言存在的原因：Agent 编写了一个脚本，脚本使用 Sabline 编写，而它声明的影响以及尚未证明的承诺应出现在 Security 选项卡中，而不是只留在审查者的脑海里。

将以下内容复制到 .github/workflows/sabline.yml：

name: sabline
on: [push, pull_request]

permissions:
  contents: read
  security-events: write     # so the findings reach code scanning

jobs:
  sabline:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5
      - uses: gowrishankar-infra/sabline-lang@c051b51c0aecefccdf90080952f6300f1362fd1a  # v8.8.0

Action 固定到某个提交，并在旁边的注释中标明其标签： 复制之后，标签可能会被指向其他代码，而提交不会。 这样固定后，它会安装该提交对应的 Sabline，就像使用标签时一样。

这就是完整的工作流。不添加 with: 块时，Action 会安装 Sabline 和证明器，检查仓库中的每个 .vel 文件；如果某个文件无法编译，或包含被证明器反驳的承诺，就会使作业失败；并使用固定到某个提交的 github/codeql-action/upload-sarif，以 SARIF 2.1.0 格式上传检查结果。私有仓库需要启用代码扫描；如果没有启用代码扫描，也没有 security-events: write 权限，请设置 sarif: "false"。对于来自 fork 的拉取请求，作业令牌无法上传，因此会跳过该步骤；文件仍会生成，其路径是 sarif-file 输出。无论哪种情况，检查结果都会打印到作业日志中。

Security 标签页中显示的内容

每个发现对应一条警报，显示在触发警报的代码行上，并链接到 错误页面中的对应行。 以下是规则 ID 及各规则的一条实际消息：

规则	级别	警报内容
E300	错误	function 'fetch' calls 'read_file' which needs effect 'fs', but 'fetch' declares no effects (it is pure)
E520	错误	'to_int' can fail - that cannot be ignored
E700	错误	promise cannot be kept: 'discount' ensures result >= 0 - proven without running the program: price = 9 gives result = -1
E701	错误	this call can break a promise: 'discount' requires price >= 0, but 'main' can call it with price = -3 - proven without running the program
unproven-promise	警告	'count_rows': ensures result >= 0 - not proven before running; checked while the program runs
contract-coverage	备注	'total' takes or returns data and promises nothing about it
capability-widened	错误	net is needed by sync.vel, not in the surface of sabline.capabilities (a new effect, net)
capability-effect-gained	错误	'main' now declares net, which it did not in sabline.capabilities: net: calls pull at line 6, which declares net
capability-narrowed	备注	surface: "net" is no longer needed——基线包含的权限超出代码所需；capabilities init --force 会记录范围更窄的权限面
dependency-capability-widened	错误	npm:mixed 0.1.0 -> 0.2.0: net:telemetry.example.net is needed by lib/report.vel (a new effect, net)
dependency-effect-gained	错误	npm:mixed 0.1.0 -> 0.2.0: 'render' now declares net: net: calls post at line 3
dependency-install-script	错误	npm:textkit 1.0.0 -> 1.1.0: an install-time script was added: npm postinstall: node setup.js [registry manifest, tarball package.json]; what it does is not derived
dependency-surface-unknown	备注	npm:textkit 1.0.0 -> 1.1.0: capability surface unknown. Neither 1.0.0 nor 1.1.0 holds a .vel file, so there is no declared capability surface to compare. ...
dependency-added	备注	npm:textkit 1.0.0 -> 1.1.0: now declares helper ^2.0.0 (dependencies); its own surface was not examined
dependency-narrowed	备注	sabline.lock:mailer 6ed598a1e2bf -> 3f7a9875d0de: surface: "net:collector.example.net" is no longer needed

编译器错误表中的每个代码都是独立规则，因此解析错误（E1xx）、未知函数（E200）或类型错误（E5xx）都会以相同方式出现；E3xx 是作用效果代码，E7xx 是证明器代码。在 check --strict 下，未证明的承诺会被视为 error，而未能证明会结束的循环则是 E612。uses-io、uses-fs 和 loop-not-shown-to-end 备注来自 sabline audit --sarif，Action 不会运行该命令；Action 会在下文的 pr-comment 中报告这些内容。dependency-* 行来自下文的 deps-diff，且仅在启用该输入时出现；每条结果都会落在锁文件中固定升级版本的那一行。

Sabline 建议的修复方案是句子，而 SARIF 的 fix 必须包含要更改的确切字节，因此这些建议会放在每条结果的 properties.fixes 中，而不是作为 SARIF 修复项，填入一个编辑内容来占位。

仓库声明的预算

sabline capabilities init 会将仓库的 .vel 文件所需的能力范围记录到 sabline.capabilities 中，包括效果、路径、主机、Python 模块、一次运行可执行的文件和网络操作数量，以及每个函数的效果；请将其提交。从此以后，Action 会在每次推送时运行 sabline capabilities check，并在任何变更需要更多能力时失败，指出扩大的能力、引入变更的文件、函数和行号，以及接受该变更所需的基线修改。这些就是上方的 capability-* 行，它们会与检查结果一起提交给代码扫描。

比较始终以该文件为准，而不是与上一次提交比较：即使能力是在许多次小提交中逐步添加、每次单独看来都不令人担忧，也会在每次提交时失败，直到有人扩大该文件；届时，变更会在评审中显现。删除 sabline.capabilities 的拉取请求也会失败，因为这会关闭递增限制；要关闭它，应在工作流中设置 capabilities: "off"，这样变更就会清晰可见。没有该文件时，递增限制就会关闭。EMBEDDING.md 说明了相关规则；check_ratchet.py 实现了这些规则，其中包括一段六次提交的历史记录，该记录只有在提交到达网络操作时才会失败。

一次升级带来了什么

依赖项在两个版本之间可能改变其功能，而名称、发布者和依赖项列表都保持不变。npm 包 postmark-mcp 就是一个有记录的案例：Koi Security 于 2025 年 9 月报告称，1.0.0 到 1.0.15 版本作为电子邮件工具正常工作，而 1.0.16 版本会将每条外发消息密送给一个外部地址。同一发布者的签名可以验证这两个版本；它们的 SBOM 列出的依赖项也相同。

sabline deps-diff 比较同一依赖项的两个版本：

sabline deps-diff dir:vendor/mailer 1.4.0 1.5.0          # a directory per version
sabline deps-diff git:https://github.com/o/mailer v1.4.0 v1.5.0
sabline deps-diff npm:some-package 1.0.15 1.0.16
sabline deps-diff pypi:some-package 2.31.0 2.32.0 --json
sabline deps-diff --against origin/main                  # every upgrade in the changed lockfiles

对于 Sabline 库，它会像 capabilities init 那样，根据每个版本的 .vel 文件计算其能力范围；再像 capabilities check 将目录与其基线对比那样，以较旧版本为基准检查较新版本，并报告较新版本新增的内容——效果、主机、路径、Python 模块、操作数量，以及声明了未声明效果的函数——并列出每项对应的文件、行号和调用：

GAINED  net:collector.example.net - not in 1.4.0's surface
    in mailer.vel
      mailer.vel:3  send calls post("https://collector.example.net/copy")
GAINED  net operations in mailer.vel: at most 2 in a run; 1.4.0 had at most 1

调用方若已为自己的请求声明了 net，则针对两个版本编译时都能通过，因此编译器不会拒绝任何一个版本；差异在于依赖项声明了什么，而这正是此命令读取的内容。基准测试的第 12 类包含 3 个这种结构的程序和 1 个对照程序。

对于 其他任何包，它只读取注册表和包归档中声明的内容，不会读取更多：npm 或 pip 在安装时运行的脚本（preinstall、install、postinstall、npm 的 node-gyp rebuild、setup.py、构建后端、会导入模块的 .pth 文件），以及每项脚本是否是新增或已更改——包括命令未变但其背后的文件已更改的情况；当注册表清单与 tarball 中的 package.json 不一致时，也会读取两边的脚本，因为 npm 运行哪一份脚本曾随 npm 版本而变化——还有声明的依赖项。它不会推断 Python 或 JavaScript 代码能做什么，也不会猜测：它会将能力范围报告为 未知，并以状态码 3 而非 0 退出。这种结果往往就是全部信息。据 Koi Security 称，postmark-mcp 的 1.0.16 版本除了新增密送副本的代码外，没有其他更改，因此 deps-diff 不会发现任何安装脚本或依赖项变化，也会将能力范围报告为未知。（npm 此后已撤下该包的所有版本；现在 deps-diff 会报告这两个版本都无法读取。）

退出码：当两个能力范围均已推导且没有新增内容时为 0；有新增内容时为 1；没有发现可见的新增内容但未推导出能力范围时为 3；无法读取某个版本时为 2。--json 输出格式为 sabline.deps-diff/1；--sarif 会写入上述 dependency-* 结果。包参数用于指定读取来源——pypi:、npm:、git: 或 dir:——不带来源的名称会被拒绝，因此绝不会将 npm 包与同名的 PyPI 包进行比较。 SABLINE_NPM_REGISTRY 和 SABLINE_PYPI_URL 可用于指定镜像。

设置 deps-diff: "true" 后，Action 会在拉取请求中运行 sabline deps-diff --against，以基准分支为参照：它会读取拉取请求更改的锁文件——package-lock.json、npm-shrinkwrap.json、requirements*.txt 中的固定版本、Pipfile.lock、poetry.lock、uv.lock、pdm.lock 和 sabline.lock；对于其中的 vendored 库，会逐个文件进行比较——比较每个已升级的依赖项，最多 30 个，并发布一条评论，说明每项依赖新增了什么；后续运行时会编辑这条评论，而不会另发评论。对于它不读取的锁文件（yarn.lock、pnpm-lock.yaml 等），评论会注明这些文件已更改但未读取。若某项依赖解析自 git、路径，或它不读取的注册表或索引，则会将其排除并说明原因，因为同名的公共包并非同一个包；所有 requirements*.txt 中指定了其他索引的固定版本也会如此处理。启用 sarif 后，检查结果会发送到代码扫描。它需要 pull-requests: write，并且绝不会导致作业失败。

Pull request 会为其工作流授予哪些权限

设置 permissions-ratchet: "true"（8.3）后，在 pull_request 事件中，Action 会运行 sabline permissions-ratchet --against，并指定 pull request 的基础提交。它会逐个作业比较 .github/workflows 中每个工作流文件在分支头部和基础提交处的 permissions: 块；只要权限范围有任何扩大，就会使作业失败，并在错误中指出文件和行号。权限范围扩大包括：某项权限的级别提高（none < read < write）；某个作业既没有自己的权限块，也没有工作流级权限块，因此会采用仓库默认的令牌权限；或者新作业或新工作流文件授予了任何权限。权限范围缩小会被报告，但不会导致失败。重命名作业会被视为删除一个作业并新增一个作业，而新作业会按无权限进行比较。此输入默认关闭。对于没有 .vel 文件的仓库，这是唯一有帮助的输入，而且无论仓库是否有 .vel 文件都会运行。如果某个工作流文件无法被可靠读取——例如包含锚点、制表符、重复键或第二个文档——该步骤会失败，而不会将其视为没有权限；无法获取基础提交时也一样。它比较的是文件，而不是 GitHub 实际运行的内容，因此不会检查作业调用的可复用工作流的权限（这些权限由该工作流自身的权限块控制）、仓库的默认令牌设置，或基础分支上的 pull_request_target 工作流副本（实际运行的是这个副本）。--json 会写入 sabline.permissions-ratchet/1，该格式目前是暂定的。

Action 还会执行的其他操作

  - uses: gowrishankar-infra/sabline-lang@c051b51c0aecefccdf90080952f6300f1362fd1a  # v8.8.0
    with:
      files: "src/*.vel"     # default: every .vel file in the repository
      version: "8.8.0"       # default: the Action's own version (8.8.0)
      proofs: "true"         # the default; installs z3-solver
      format: "true"         # also fail if the code is not canonically formatted
      min-proven: "80"       # fail below this percent of promises proven
      pr-comment: "true"     # audit every changed .vel on the pull request
      sarif: "true"          # the default; findings to code scanning
      capabilities: "check"  # the default once sabline.capabilities exists
      deps-diff: "true"      # comment on what each upgraded dependency gained

在 pull_request 事件中设置 pr-comment: "true" 后，Action 会发布一条评论，其中包含 pull request 所改动的每个 .vel 文件的 sabline audit 结果——包括效果、触及的 Python 模块、已证明安全的部分、安全命令，以及诸如循环未能证明会终止之类的警告；后续运行会编辑同一条评论，而不是再添加一条。评论还会附上权限棘轮的结果，以及分支相对于基础分支的 sabline review 结果：范围、已证明安全的部分、新增的易出错函数、新增的主机和路径，以及仅根据这些事实计算出的单词风险等级。它使用作业自己的 GITHUB_TOKEN 通过 REST API 操作，因此作业需要 permissions: pull-requests: write。无论检查是否通过，都会发布审计结果；无法编译的文件也会据实报告。

不使用 Action 时，同一份 SARIF 也可供 SonarQube（sonar.sarifReportPaths）、Azure DevOps 或其他读取该格式的工具使用：

sabline check src/*.vel --sarif > sabline.sarif   # exit 1 as the plain check
sabline proofs src --sarif > proofs.sarif         # promises left to runtime
sabline audit src --sarif > audit.sarif           # what each function may touch
sabline capabilities check --sarif > caps.sarif   # what widened past the baseline

一次运行，驱动程序为 Sabline，并附带其版本；错误表中的每个代码以及非错误类发现项都有对应规则。每条结果都包含文件、行号和 Sabline 的消息。

或者无需安装任何东西：

docker run --rm -v "$PWD:/work" sabline check /work/main.vel

允许 Agent 编写的 Sabline 运行之前，审查者应先阅读：THREAT_MODEL.md、COMPLIANCE.md 和 SECURITY.md 中的验证步骤。incidents/ 则从另一面提出同一个问题：自 2023 年以来，该领域公开报告的攻击；每种攻击都以 Sabline 程序的形式描述，并给出它是否会拒绝的判断——包括那些诚实结论为不会拒绝的情况。这是一份攻击模式目录，并不声称 Sabline 能防止真实事件。

项目

路线图 · 支持与预期 · 编译器的工作原理 · 维护者 · 安全策略 · 稳定性 · 更新日志

由一人以开源方式维护，并在 SUPPORT.md 中明确说明其局限。

引用此代码库

作者为 Palakurthi Gowri Shankar（姓氏为 Palakurthi）。 CITATION.cff 中包含引用信息，GitHub 会在文件列表旁提供“引用此代码库”选项。一篇介绍 Sabline 的预印本即将发布；在发布之前，请引用此代码库。能力格式的引用信息单独列出，见 sabline-spec 自身的 CITATION.cff。PROVENANCE.md 记录了日期和存档标识符。

参与贡献

实现位于 sabline/ 包中，每个阶段对应一个易读的模块，按流水线顺序排列——从词法分析器到命令行；sabline.py 负责启动。请先阅读 ARCHITECTURE.md，了解各部分如何协同工作；再阅读 MAINTAINERS.md，了解评审流程。

想从某处开始？ 请查看 适合新手的问题 ——这些是小型、独立的任务，每项都注明了要查看的文件以及“完成”的标准。

examples/ 中有 97 个示例程序，由 run_tests.py 运行，每个程序都带有预期判定结果；其中 36 个是刻意设计为被拒绝的——每次拒绝都能证明一项保证。任何更改发布之前：

python run_tests.py                 # every example, expected verdicts
sabline test examples/std_test.vel  # the library's own tests
python fuzz_native.py 60            # both engines must agree
sabline fmt examples/*.vel stdlib/*.vel --check

许可证

MIT © Palakurthi Gowri Shankar