证据 · 615E501 · 2026-10-06

v0.8.0 实现了什么，又没有证明什么。

每项证据都有状态、范围和复核日期。

0.8.0 对应提交 615e501，在确切标签的 82 个作业全部通过后，于 2026 年 10 月 6 日发布。实现包含源码定律、更丰富的 Rust 集成、连接编译器的开发工具和经检查的开发重载。下表将每种可用配置与其尚未满足的完整产品要求和支持要求分开记录。

semaprax://evidencev0.8.0

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 目前实现了什么？

此版本提供经过检查的源码与语义修改、类型化运行时智能体、范围明确的 Lean/Z3 定律证明、选定 Rust API 与生成的适配器、同线程 Future、开发工具提供方与技能、热重载开发会话、token 报告，以及压缩包签名来源证明。确切标签 CI、针对性的本地测试和应用实测回答的是不同问题。完整目标矩阵仍有 55 项 Partial 要求；这一总数并不意味着各个已实现配置缺失。

// 01

能力证据台账

当前状态	源代码状态	证据与来源	发布状态	支持范围	证据
规范源码与稳定身份 `stable-semantic-program-graph`	部分	确切标签的 Project 与 Rust 作业通过准入语义图契约；完整语义基础目标仍为部分完成。	有界 beta 源码/工具链配置	可读 `.spx` 仍是 Git 中的规范表示。显式 `@id` 在受支持的显示名称修改后继续标识同一声明。修订绑定规范源码和编译器隐式 prelude，而非偶然的源码位置或图传输格式。	GitHub 仓库
受限上下文与紧凑投影 `bounded-agent-context`	部分	已实现范围明确的类型化上下文、紧凑重放，以及已提交的本地分词器比较。	有界 beta 源码/工具链配置	选择确切的图或任务上下文，并限制深度、方向、节点数和字节数。model-text v2 在部分大型输入上减少 token，在小型输入上则会增加；报告保留分词器与比较边界。	GitHub 仓库
语义修改，而非任意重写 `revision-bound-semantic-patches`	部分	确切标签的源码修复与 Project 作业通过有界修改契约；任意仓库重写不在范围内。	有界 beta 源码/工具链配置	检查上下文、派生候选、预览影响、审阅、重放检查，然后显式授权应用。操作家族已超出重命名，包含有边界的表达式替换、结构修改及指定的 rebase/merge 组合。各协议保留独立的修订、身份与操作限制。	GitHub 仓库
受控发布是独立边界 `managed-workspace-semantic-operations`	部分	Project 产品验收在 Linux、macOS 与 Windows 通过；发布仍需显式授权。	有界 beta 源码/工具链配置	受管工作区代、候选证据、Project 修订存储与 MCP 工作流保留显式写入和发布权限。多文件验证不等于任意原始路径、Git 或编辑器的原子更新。Rust 嵌入 API 提供输入上限、取消与不透明会话，并非无限制宿主访问。	GitHub 仓库
可重放的语义证据 `semantic-evidence-capsules`	部分	修订绑定证据已实现且发布声明核对通过；回执不授予修改权限。	有界 beta 源码/工具链配置	证据将已检查事实与候选修改绑定到源码和修订。回执可支持审阅或拒绝，但不会授予执行、修改或发布权限。	GitHub 仓库
多模块项目与离线脚手架 `bounded-multi-file-project`	部分	Project Manifest、产品验收及已安装工具链旅程作业通过；服务宿主范围另行限定。	有界 beta 源码/工具链配置	清单定义声明的源码、入口、测试与导出。内置计算器、库和服务模板各有其配置。new 使用编译进工具的文件创建全新项目；源码检查、解释执行测试与目标构建遵循选定清单的契约。	GitHub 仓库
解释器、原生与 Core Wasm 执行 `native-and-wasm-lowering`	部分	三个目标工具链包及选定原生/Wasm 门槛通过；各运行配置仍有各自准入限制。	有界 beta 源码/工具链配置	已获准的标量、拥有所有权数据、泛型、集合和不可变列表配置，可通过解释器、原生 C11/Clang 与 Core Wasm 执行，并各有一致性检查。显式启用的智能体阶段宿主单独绑定；普通 yield 仍不允许生成原生/Wasm 输出。	GitHub 仓库
有界标量 JavaScript/TypeScript 导出 `public-wasm-scalar-exports`	部分	确切标签的 Chromium 标量导出作业通过；其他浏览器与拥有数据包另行处理。	有界 beta 源码/工具链配置	稳定 ID 标量导出具有独立公共 Wasm 配置和浏览器测试样例。拥有数据包、广泛浏览器支持、组件及泛型签名各有契约，不能继承这一支持声明。	GitHub 仓库
类型化运行时智能体 `bounded-agent-runtime`	部分	AGENT-06 生命周期与客户端作业已在 Linux、macOS 和 Windows 上通过。默认在线路径仍选择解释器；显式启用、由调用方持有的目标宿主具有独立且范围明确的证据。	有界 beta 源码/工具链配置	类型化源码角色驱动初始化、观察、模型提案、授权、副作用与归约。绑定的 Proposal 模式约束解码。默认在线路径使用解释器；选定库路径可提供持有的原生 C11/Core Wasm 阶段宿主，并遵循其本地一致性与恢复检查。	GitHub 仓库
所有权与可重放清理 `ownership-inspired-memory-management`	部分	GEN-05B 与 Rust 作业通过准入所有权配置；通用生命周期安全仍待完成。	有界 beta 源码/工具链配置	拥有所有权和借用的值、清理计划、选定记录/变体与资源组合均可执行。范围明确的拥有所有权的 Bytes、标量快照、事务式可变和同步借用文本回调，具备移动、逃逸与清理控制。通用生命周期、任意捕获结构和公共借用 ABI 尚未完成。	GitHub 仓库
更广的日常编程能力 `everyday-language-and-collections`	部分	确切标签的 STD-08 标准库作业通过；完整 Everyday 库及物理提供端仍待完成。	有界 beta 源码/工具链配置	记录、变体、类、继承、限定的泛型推断、Option/Result、可变操作、循环、向量、迭代器、函数值和有界闭包，可用于实际程序。不可变 List<i64> 增加持久化构造器与绑定源码的定律示例；更广泛的约束和功能组合仍有限制。	GitHub 仓库
预算、持久恢复与模型调用 `model-budgets-and-durable-recovery`	部分	AGENT-06 作业通过有界生命周期与记账路径；服务商账单和宿主策略仍属外部事实。	有界 beta 源码/工具链配置	显式宿主适配器提供凭据、传输和存储。限制可涵盖调用、token、字节、截止时间和报价成本。持久配置先确认意图再分派，并拒绝不确定的重复派发。通用宿主配置支持有界重试/故障转移；绑定源码模型路线不会自动重试或切换服务商。观测用量不等于保证账单正确。	GitHub 仓库
应用与经济智能体实验 `application-and-economic-agent-profiles`	实验性	范围明确的参考快照宿主，具备本地打包和选定托管 Linux/Podman 证据；经济智能体权限仍须显式提供。	有界 beta 源码/工具链配置	参考服务路径将经过检查的会话、任务与作业决策，同快照持久化及选定 JSON 事件或 OTLP 遥测组合起来。SQL 适配器会被拒绝。经济智能体保留显式的钱包、模拟、批准、签名和对账职责，不能据此保证外部操作恰好执行一次。	GitHub 仓库
生成边界仍按配置限定 `owned-data-package-previews`	开发者预览	Project 产品验收及原生 Rust SDK 在三个宿主通过；生成包发布仍未决定。	生成/私有预览；发布与公共支持需分别决定	Project v8 承载 Bytes 及选定 Option/Result 形式；v9 增加平面拥有记录，v10 增加拥有 UTF-8，v11 增加嵌套拥有记录。生成的 native/Rust、npm/Wasm 消费端、私有传输与公共泛型元数据各有契约。工具链发布、包发布与公共支持是不同决定。	GitHub 仓库
广泛原生与应用支持 `broad-platform-support`	路线图	三种工具链包已发布，且存在有界浏览器/移动/桌面配置。跨浏览器引擎、物理设备、操作系统和安装流程的完整受支持应用平台仍属更广产品要求。	尚未建立完整支持	三种工具链包已发布，且存在有界浏览器/移动/桌面配置。跨浏览器引擎、物理设备、操作系统和安装流程的完整受支持应用平台仍属更广产品要求。	GitHub 仓库
通用双向生态互操作 `bidirectional-ecosystem-interoperability`	路线图	通用所有权安全外部接口、稳定聚合/资源/组件/泛型 ABI、持续维护包发布及广泛宿主语言兼容仍未完成。元数据、生成代码和私有宿主样例不能完成此要求。	尚未建立完整支持	通用所有权安全外部接口、稳定聚合/资源/组件/泛型 ABI、持续维护包发布及广泛宿主语言兼容仍未完成。元数据、生成代码和私有宿主样例不能完成此要求。	GitHub 仓库
签名发布来源证明 `release-provenance`	已演示	确切发布作业签署汇总来源证明，独立验证签名文件集，并发布三个工具链包的证明文件。	Beta 工具链和来源证明文件已发布	已证实工具链包完整性与签名构建来源；未证实公证、跨宿主可复现性或当前撤销状态。	GitHub 仓库
编译器生成的泛型目标边界 `public-generic-compiled-boundaries`	开发者预览	确切标签的泛型门槛在 Linux、macOS 和 Windows 通过；私有已检查 Core Wasm 提供端、TypeScript 载体及原生结算语料可执行。	未发布的私有配置；PG-9 仍不支持	一个准入泛型端点和有界消费端、结算案例已实现。更广端点形式、公共 ABI 与包发布仍待完成。	GitHub 仓库
显式启用的原生与 Wasm 智能体阶段 `source-agent-target-parity`	开发者预览	范围明确的源码智能体阶段通过封装的解释器、原生 C11 和 Core Wasm 路径执行，并具有选定的本地一致性、恢复和迁移检查。	显式库目标选择器；默认在线路径仍选择解释器	宿主显式提供所持有的原生或 Wasm 运行时。这并不证明通用指令计量、不受限的清理或终结器一致性、全部源码配置，或广泛部署/托管环境中的智能体目标支持。	GitHub 仓库
有界源码 yield 与持久化续体 `bounded-resumable-effects`	实验性	解释器配置接受顺序及依赖控制流的 yield、选定的拥有所有权的 Bytes 传递，以及经过认证的持久化源码恢复。公共拥有所有权的智能体子集具备两轮和选定进程重启检查。	没有公共原生/Wasm 续体 ABI	每种配置限制挂起点、拥有所有权的状态和恢复阶段。普通原生/Wasm 生成器仍拒绝含 yield 的函数。通用调度、任意拥有所有权的续体、通用迁移和稳定公共续体 ABI 尚未完成。	GitHub 仓库
本地签名 Registry-v3 信任检查 `signed-registry-local-trust`	实验性	由生产者绑定的根与叶、签名元数据、保留代、锁绑定产物读取及缓存桥接已有专项本地门槛。	没有托管注册表或公共分发	本地签名证据不授予隐式抓取、执行或包发布权限。生产根密钥、网络传输与支持仍须分别处理。	GitHub 仓库
固定版本 Lean 证明与义务门槛 `lean-kernel-obligation-gate`	已演示	确切标签的托管 Lean 作业通过 Kernel-0 证明、公理审计、生成义务导出与差分语料。	有界研究证明，并非通用安全证书	证明只覆盖形式化 Kernel-0 子集，不覆盖整个语言、所有后端或漏洞不存在性。	GitHub 仓库
源码定律与证明重放 `source-laws-and-proofs`	部分	原生定律语法、选定定律清单、受保护修复，以及范围明确的已安装 Lean/Z3 配置，均具备可执行的正向与变异/拒绝证据。	范围明确的源码与证明工具配置	契约、关系、模标量、有限结构、协议和不可变列表定律保留确切源码与证明身份。不受支持的目标保持待解决或被拒绝状态；编译降级、外部内部实现和外部副作用，不属于一般性证明主张。	GitHub 仓库
丰富的原生 Rust 集成 `native-rust-rich-interop`	开发者预览	已提供选定导入、生成的所有权/视图/回调，以及真实 Regex/Url、Serde/迭代器和 reqwest/Tokio 应用检查。	生成的开发者预览；选定原生签名	绑定所有者的视图，以及范围明确的 FnOnce、FnMutI64 和同步借用文本捕获，保留各自的生命周期与回滚契约。应用回执同时记录吞吐量退步和客体/宿主限制；尚未证明任意 crate、ABI 或零开销支持。	GitHub 仓库
同线程 Rust Future `local-rust-futures`	开发者预览	生成的本地 Future 句柄、选定源码 yield、调用方拥有的执行器，以及真实 HTTP、取消和关闭控制，均具有本地证据。	有界本地生成配置与按 Project 选择的配置	宿主提供执行器与运行时。一个已获准的源码挂起点及确切 Project 修订绑定到生成的适配器；流、跨线程执行、任意 Future 状态的持久化和通用异步导入，仍属于独立范围。	GitHub 仓库
连接编译器的开发工具 `compiler-assisted-harness`	实验性	任务/计划/修复反馈、提供方锁定与信任、检索、官方技能、模型路由及桥接/MCP，具有本地和选定托管 Linux 证据。	完整工具链 harness 与独立宿主；显式项目配置	按项目选择的 Graft/Graphify、RTK 视图和 Ponytail/Caveman 技能，支持范围明确的工作流。WikiSkill 演进和路由资格评测均有显式检查。Windows、更广泛的模型/平台结果，以及自动更改默认配置，都需要更多证据。	GitHub 仓库
经检查的开发热重载 `checked-hot-reload`	开发者预览	持续保留的解释器会话与 VS Code 控件，已通过选定 macOS arm64 激活、拒绝、安全点和生命周期检查。	有界本地 dev 会话；源码智能体迁移属于独立路径	候选修改在激活前接受检查，无效编辑不会影响当前修订的可用性。已记录的小型测试用例中，重载比重启更慢。其他操作系统、原生/Wasm 状态切换和生产部署，不在此结果的证明范围内。	GitHub 仓库
上下文、token 与任务成本核算 `task-token-accounting`	部分	已实现确切本地分词器报告、会话汇总与标准化提供方回执；已记录的付费试验未达到更改默认配置的要求。	本地测量与显式提供方用量核算配置	分别保留可比较的选定载荷、分词器指纹、预留量、观察用量，以及报告或估算的金额。缺失用量保持不可用状态，失败调用也保留在核算中。已记录的最佳节省未达到声明门槛。	GitHub 仓库