规范源码与稳定身份
可读的 .spx 仍是 Git 中的规范表示。显式 @id 让声明在受支持的显示名称变更后保留身份。编译器生成的修订绑定源码与选定前导库；图编码展示这些事实，并不替代源码。
架构 · 源码、语义与权限
让智能体直接查询程序模型，无需从文本重新推断语义。
先稳定身份，再修改源代码。
语义程序图让声明、类型、副作用、契约、所有权与调用关系都能通过稳定身份查询。0.8.0 将这一模型扩展到源码定律、受保护的实现修复、更丰富的 Rust 边界，以及开发工具。
entity Semaprax
status Beta 测试版
snapshot 615e501
authority github.com/wavect/semaprax// 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 检查可读的 .spx 源码，并将其解析为 HIR，即带有类型信息的编译器表示。源码身份与语义身份将查询、定律义务、候选修改和执行绑定到被检查的程序。编码智能体可以使用这一核心周围的开发工具；运行时智能体则在显式提供的宿主能力下，分别解码提案、授权副作用并归约状态。
// 01
先稳定身份，再修改源代码。
受限上下文与紧凑投影
选择声明、方向、深度、节点数与字节上限。任务上下文以及文本、二进制或模型文本投影，都保留对选定事实的确切重放。原生语义上下文代理可以借助 Graft 或 Graphify 导航仓库，但不会将外部索引当作编译器事实。
源码定律与受保护的实现修复
原生 law 声明为契约要求与关系要求提供持久身份。单独选定的 LawSet 固定完整定律清单和严格策略。已安装的 Lean/Z3 适配器可证明已获准的标量、模运算、结构化和列表定律；过期、不受支持、未知和已被反证的结果保持区分。候选修复必须满足受到保护的需求。
带修订检查的语义修改
检查上下文、生成候选修改、预览影响与审阅结果、重放检查，然后授权应用。范围明确的表达式替换、结构化编辑和指定组合，各自保留操作与修订限制。源码定律编辑和实现修复遵循不同的保护规则。
受管理的发布与嵌入
受管理的工作区代次、候选证据和 Project 修订存储，将发布绑定到经过检查的候选版本。Rust 嵌入 API 提供范围明确的输入与不透明会话。仅通过多文件验证，并不会修改任意文件、Git 引用或编辑器缓冲区。
日常语言功能与集合
已获准的配置包括记录、变体、类、继承、带限定参数推断的泛型、Option/Result、循环、迭代器、函数值、字符串和字节。不可变 List<i64> 增加持久化 nil/cons/uncons 操作。一般约束与任意功能组合仍需各自的准入规则。
所有权与回调生命周期
拥有所有权的值、借用视图、清理计划及选定的资源组合均可执行。限定的闭包配置包括拥有所有权的 Bytes 捕获、复制的标量快照、事务式可变标量状态，以及同步借用文本捕获。每种配置分别检查逃逸、移动、回滚和清理规则；更广泛的生命周期关系仍待扩展。
受显式边界契约约束的 Rust API
预先准备的 Rust API 索引选择受支持的导入和确切 Cargo 输入。生成的所有权、借用视图与回调适配器，将经过检查的源码连接到真实的 Regex/Url 和 Serde/迭代器使用方。同线程 Future 桥接使用调用方拥有的执行器。外部假设保持显式；生成的连接代码并不能证明 crate 内部实现。
类型化运行时智能体
初始化、观察、提案、解码、授权、执行与归约。每轮重新授权，归约器选择 Continue、Complete、Suspend 或 Fail。默认在线路径使用解释器；显式启用的库路径接受调用方持有的原生 C11 或 Core Wasm 阶段宿主，其本地一致性证据有明确范围。
预算、持久化恢复与模型调用
显式适配器提供传输、凭据与存储。持久化配置在分发前确认意图，并将未解决的尝试保留为不确定状态。限制与回执区分调用、工作量、字节、token 和成本。通用宿主重试/故障切换与绑定的源码模型路径具有不同契约；后者不会自动切换提供方，也不会重试结果不确定的工作。
可恢复源码与拥有所有权的续体
解释器支持范围明确的顺序及依赖控制流的 yield、选定的拥有所有权的 Bytes 传递，以及经过认证的持久化源码配置。公共拥有所有权的智能体子集具有两轮生命周期和选定的进程重启验证。普通原生/Wasm 生成器仍拒绝包含 yield 的函数；通用调度器和统一续体 ABI 尚未完成。
连接编译器的开发工具
完整工具链的 harness 协调显式任务、编译器反馈、提供方描述、按项目锁定与信任、模型路由、技能和桥接。官方 Ponytail/Caveman 技能包、Graft/Graphify 适配器与 RTK 模型视图服务于选定工作流。具有权威性的命令结果与供模型阅读的紧凑输出保持分离。
经检查的开发重载
持续保留的解释器会话检查候选修改、规划兼容性，并在调用之间激活修改。轮询监视声明的 Project 输入；无效修改不会影响当前修订的可用性。VS Code 控件展示当前、待激活和未提交状态。源码智能体日志迁移属于完整工具链中的独立路径。
应用与经济智能体配置
参考服务将经过检查的会话、任务与作业决策，同快照宿主、显式 HTTP/TLS 以及选定的 JSON 事件或 OTLP 遥测组合起来。已通过的 Linux/Podman 流程仍有明确范围；SQL 适配器会被拒绝。经济智能体保留由宿主负责的钱包、批准、签名和对账边界。
生成的包与本地注册表信任
拥有所有权数据的 Project 配置，以及一个由编译器生成的私有泛型 Wasm 端点，都具备生成使用方的验证证据。公共泛型接口仍不受支持，也未发布。本地签名注册表元数据、持有的代次与锁定读取，本身不提供托管包注册表或网络获取权限。
证明与发布来源
确切标签的 Lean 作业检查其范围明确的形式化内核与证明义务导出。发布作业另行证明三个压缩包的构建，并签名、验证汇总来源证明。这是不同的证据链；二者都不证明整门语言的正确性、公证状态或跨宿主构建可复现性。
// 02
源代码投影保持可读
module examples.meaning;
@id("math.add")
fn add(left: i64, right: i64) -> i64
requires left >= 0
requires right >= 0
ensures result == left + right
{
left + right
}
@id("app.main")
fn main() -> i64
ensures result == 42
{
add(19, 23)
}本页依据 v0.8.0 标签及其固定源码提交审阅。版本化规范定义准入范围与权限；矩阵和路线图中的旧发布标题属于历史记录。 GitHub 仓库.
// DOCS
阅读 Semaprax 手册
在线手册是从 main 发布的英文指南，可能包含 0.8.0 之后的变更。复现本次发布时，请使用固定提交的手册快照。
// REF
本页一手来源
本页依据 v0.8.0 标签及其固定源码提交审阅。版本化规范定义准入范围与权限；矩阵和路线图中的旧发布标题属于历史记录。
// FAQ
常见问题与实用解答
语义图是知识图谱或 RAG 系统吗？
核心图由编译器从经过检查的源码生成，包含稳定声明、类型、契约和关联。开发工具还可以使用 Graft 或 Graphify 导航仓库。这些外部索引补充编译器的语义事实，并不替代修订与验证规则。
智能体能通过语义补丁编辑任意程序吗？
工具链提供特定的、绑定修订的编辑操作、候选修改审阅与重放检查。受保护的定律清单将需求与可编辑的实现体分开。智能体必须使用已获准操作和已授权应用路径；上下文查询或成功证明，并不意味着有权覆盖任意文件。
Wavect 研究项目: Wavect GmbH. 由 Wavect 创建的开源系统研究项目。