与源码一同维护的定律
声明稳定的定律，选择证明清单，并重放受支持的 Lean/Z3 证明义务。在保护预期需求的同时修复实现体。
证据V0.8.0 BETA · APACHE-2.0
为编码智能体构建，也让人类读得懂的系统语言。
源码可读，语义可查，修改可验证。
让编码智能体了解代码背后的类型、契约与关联。Semaprax 0.8.0 在同一套 Beta 工具链中整合了源码定律与证明工具、更丰富的 Rust 集成、开发工具、经检查的热重载，以及任务级 token 报告。从一个小程序入手，再连接项目需要的功能。
revision sha256:<program-state>
query app.main --depth 1
context typed · bounded · stable-id
patch expected_revision == current
verify fail_closed
target native | browser/wasm// STATUS
审计快照中的仓库状态
| 仓库快照 | 615e501 · 2026-10-06. v0.8.0 标签指向固定的源码提交。该标签的确切 CI 已成功完成，但不构成全面的生产可用性或安全保证。 |
|---|---|
| 完整产品状态 | 55 部分 · 0 已实现 · 0 缺失 |
| 语义图与项目契约 | 规范源码、稳定 ID 和经过检查的编译器表示，将定律、语义查询、修改与执行连接起来。按功能选择的图模式和 Project 模式，各自保留独立的准入、兼容性和宿主权限契约。 |
| 已发布的 Beta 版本 | v0.8.0 · 发布于 2026 年 10 月 6 日 07:37 UTC。确切标签的 82 个作业全部成功。已发布三个工具链包、SHA256SUMS、各包的构建证明和签名汇总来源证明。发布作业在发布前独立验证了签名文件集。工具链包未经过公证，也不声称构建可复现；离线验证不能确认当前的撤销状态。 确切标签 CI. |
| 包与 API 预览 | 此版本包含可用的语言、定律、开发工具和宿主集成配置。生成的 Rust/npm 包、公共泛型 ABI 及更广泛的平台支持，仍须分别决定其发布与支持范围。 |
什么是 Semaprax？
Semaprax 是一种开源、面向智能体的系统编程语言，目前处于 Beta 阶段。可读的 .spx 源码保留在 Git 中，编码智能体可以查询类型化的程序语义、检查源码定律，并针对确切修订提出修改。0.8.0 还提供类型化运行时智能体、与编译器连接的开发工具，以及范围明确的 Rust、原生和 WebAssembly 集成。
// v0.8.0
v0.8.0 的重要变化
0.8.0 源码与已发布 Beta 工具链中的六项实用进展。
更丰富的 Rust 集成
选定的 Rust API、生成的所有权与回调适配器，以及真实的 Regex/Url、Serde/迭代器和 Tokio/reqwest 应用，将集成能力扩展到标量演示之外。
证据与编译器连接的开发工具
将语义上下文与按项目选择的提供方、Graft/Graphify、RTK 视图、官方 Ponytail/Caveman 技能和显式模型路由策略结合起来。
证据经检查的开发重载
dev 命令与 VS Code 控件会验证候选修改，等待安全的激活边界，并在编辑无效时保留正在运行的程序。
证据Token 与任务成本报告
比较确切的上下文载荷，检查会话中的 token 增减，并区分提供方回执、预留用量与估算成本。
证据经过验证的发布文件集
确切标签的 82 个作业全部通过。三个预编译包附带校验和、构建证明，以及经过独立验证的签名来源证明。
证据// v0.8.0
想直接使用预编译命令行工具？
0.8.0 提供适用于 Apple Silicon macOS、Linux x86-64 GNU 和 Windows x86-64 MSVC 的压缩包。此版本没有图形安装程序。每个包都包含以 semaprax 命名的完整工具链、semapraxd 和一个冒烟示例。从源码安装时，完整构建使用独立名称 semaprax-full。
- 选择与操作系统和 CPU 匹配的压缩包。GitHub 的 Source code 下载项是仓库快照，不是预编译可执行文件。
- 解压适用于你所在平台的归档文件前，请核对 SHA256SUMS。将解压后的目录加入 PATH，或使用完整路径运行 semaprax。
- 运行
semaprax --version，然后在解压目录中检查并运行附带的smoke/meaning.spx。其返回值为 42。原生构建需要 Clang；Web 示例使用 Node.js 22+。 - 验证签名来源证明时，请将三个平台的全部归档文件及签名元数据放入同一目录，再按链接中的说明运行
semaprax release verify <release-dir>。结果必须确认已完成离线密码学验证；无签名验证成功并不表示签名有效。
SHA256SUMS · 校验和与签名来源证明 · 发布清单 · 发布记录
// CLI
运行第一个经检查的程序
此源码方式固定到已审阅提交，需要 Git 和 Rust/Cargo 1.88+。Cargo 首次运行可能下载依赖。这两个 check/run 命令无需 Clang、Node.js 或 AI 服务商；程序返回 42。
git clone https://github.com/wavect/semaprax.git
cd semaprax
git checkout --detach 615e501612895a52b3fdd72a03baf875a8f0df1b
cargo run --locked -p semaprax -- check examples/meaning.spx
cargo run --locked -p semaprax -- run examples/meaning.spx// PROJECT
安装一次，即可创建项目
在同一个固定提交的仓库检出目录中继续操作。Cargo 安装独立 CLI；下方 PATH 设置适用于 Bash 和 Zsh。生成的计算器项目包含源码、清单、测试和 AGENTS.md。请选择全新的目标目录；new 使用内置文件，不会初始化 Git，也不会连接包注册表。
cargo install --locked --path . --bin semaprax
export PATH="$HOME/.cargo/bin:$PATH"
semaprax --version
semaprax new first-semaprax
semaprax check first-semaprax/semaprax.toml
semaprax test first-semaprax/semaprax.toml
semaprax run first-semaprax/semaprax.toml// AGENT
为编码智能体提供明确的起点
从仓库根目录出发，通过稳定身份检查同一个程序。图、上下文和已安装的语言帮助都是只读起点。之后进行语义修改时，仍需要当前修订、受支持的操作，以及明确的应用步骤。
semaprax graph examples/meaning.spx
semaprax context examples/meaning.spx app.main --depth 1 --max-bytes 65536 --max-nodes 256
semaprax context examples/meaning.spx math.add --depth 1 --filters contracts
semaprax help language
semaprax help diagnostic SPX-T208// 01
一个程序，三个相连的工作界面
开发者编辑可读源码，工具查询经过检查的语义，受支持的目标执行已获准的程序。每种目标和集成都明确说明其接受的语言功能。
- 可读源码规范 .spx 文件、稳定声明 ID、契约、定律与显式所有权。普通 check 和 run 命令无需模型账户。
- 供工具使用的已检查语义编译器生成的上下文、影响分析、候选修改审阅与证明义务。开发工具可在这一语义核心之外，接入选定的检索、技能和模型提供方。
- 受控执行解释器、已获准的 C11/Clang 与 Core Wasm 配置，以及类型化运行时智能体。智能体的模型提案须先通过确定性的授权检查，才能执行副作用。
Semaprax 语义程序图: Semaprax 检查可读的 .spx 源码，并将其解析为 HIR，即带有类型信息的编译器表示。源码身份与语义身份将查询、定律义务、候选修改和执行绑定到被检查的程序。编码智能体可以使用这一核心周围的开发工具；运行时智能体则在显式提供的宿主能力下，分别解码提案、授权副作用并归约状态。
// 02
让每次修改提案都更容易检查
稳定身份让智能体准确定位声明，范围明确的上下文解释其作用。契约和单独选定的定律约束实现，候选修改审阅与重放检查则在应用前验证修改。开发工具记录实际用量和任务结果，让效率主张接受证据检验。
衡量实际结果
减少修复歧义，分别检查任务成本与正确性
// 03
按你需要解决的问题深入了解
手册提供操作步骤，架构页解释编程模型，证据页记录已实现配置，基准页展示测量结果，互操作性页说明如何接入现有技术栈。
// 04
能力证据台账
| 当前状态 | 证据状态 | 范围 | 证据 |
|---|---|---|---|
| 规范源码与稳定身份 | 部分 | 可读 `.spx` 仍是 Git 中的规范表示。显式 `@id` 在受支持的显示名称修改后继续标识同一声明。修订绑定规范源码和编译器隐式 prelude，而非偶然的源码位置或图传输格式。 | GitHub 仓库 |
| 受限上下文与紧凑投影 | 部分 | 选择确切的图或任务上下文，并限制深度、方向、节点数和字节数。model-text v2 在部分大型输入上减少 token，在小型输入上则会增加；报告保留分词器与比较边界。 | GitHub 仓库 |
| 语义修改，而非任意重写 | 部分 | 检查上下文、派生候选、预览影响、审阅、重放检查，然后显式授权应用。操作家族已超出重命名，包含有边界的表达式替换、结构修改及指定的 rebase/merge 组合。各协议保留独立的修订、身份与操作限制。 | GitHub 仓库 |
| 受控发布是独立边界 | 部分 | 受管工作区代、候选证据、Project 修订存储与 MCP 工作流保留显式写入和发布权限。多文件验证不等于任意原始路径、Git 或编辑器的原子更新。Rust 嵌入 API 提供输入上限、取消与不透明会话，并非无限制宿主访问。 | GitHub 仓库 |
| 可重放的语义证据 | 部分 | 证据将已检查事实与候选修改绑定到源码和修订。回执可支持审阅或拒绝，但不会授予执行、修改或发布权限。 | GitHub 仓库 |
| 多模块项目与离线脚手架 | 部分 | 清单定义声明的源码、入口、测试与导出。内置计算器、库和服务模板各有其配置。new 使用编译进工具的文件创建全新项目；源码检查、解释执行测试与目标构建遵循选定清单的契约。 | GitHub 仓库 |
// DOCS
阅读 Semaprax 手册
在线手册是从 main 发布的英文指南，可能包含 0.8.0 之后的变更。复现本次发布时，请使用固定提交的手册快照。
// REF
本页一手来源
本页依据 v0.8.0 标签及其固定源码提交审阅。版本化规范定义准入范围与权限；矩阵和路线图中的旧发布标题属于历史记录。
// FAQ
常见问题与实用解答
Semaprax 可以用于生产吗？
0.8.0 是采用 Apache-2.0 许可证的 Beta 版本，于 2026 年 10 月 6 日发布。你可以安装、运行程序并探索已实现配置。确切标签发布成功并不代表生产支持；完整目标矩阵仍记录 55 项 Partial 要求。
Semaprax 只面向 AI 智能体吗？
无需 AI 模型或账户，也可以编写、检查和运行普通 .spx 程序。编码智能体通过工具使用语义上下文和受支持的修改；源码定义的运行时智能体，则是独立的类型化编程抽象。英文手册分别介绍这两种用途。
你的 AI 产品是否需要这种证据优先的工程方式？
查看 Wavect 的 AI 工程服务。由 Wavect 创建的开源系统研究项目。 GitHub 仓库. 本页依据 v0.8.0 标签及其固定源码提交审阅。版本化规范定义准入范围与权限；矩阵和路线图中的旧发布标题属于历史记录。