ZeframLou

Q: 看看这个： ZeframLou/zklean 有没有什么值得借鉴 A: -----------------cc------------------------------------- 这个项目很新（10-23 创建，0 star，作者是以太坊开发者 ZeframLou），但它几乎就是我们链条两端的一个轻量版，非常值得对照。 它在做什么：把 Lean 证明变成一个 约 1 KB 的证书，任何人不用装 Lean、一秒以内就能验证。实现方式： - 用 lean4export 导出声明 → 用 Nanoda（一个 Rust 写的 Lean 内核检查器）检查 → 整个检查过程放进 SP1 零知识虚拟机（RISC-V）里跑 → 生成一个 356 字节的 Groth16 SNARK → 用 TypeScript 写的验证器去验证。 - 生成一次证书要 5 到 20 分钟、约 20 GB 内存，第一次还要下载 6 GB 的电路文件。 值得借鉴的： 1. 对外讲法极其清楚，而且不绕圈子："发布时附一个证书，依赖你的团队每次升级一秒验完，不用重建你的 Lean 项目。"这正是我们"方式 A：不装 Lean 也能检查"的产品形态，可以直接作为我们对外定位的参照，你之前要求定位"得让外部的人明白"。 2. 指纹 = 定理陈述 + 它引用到的所有定义，不包括证明，所以"改个名字也藏不住改动"。这和 v0.2 里的 stmt_q 完全一致（名字不等于身份），算是印证了我们的设计。 3. "钉住需求"的工作流：下游团队审查一次自己依赖的那些定理，记下它们的指纹；以后每次上游发布，只需验证新证书、比对指纹。这正是包图里"按事实依赖"的样子：一个包依赖另一个包的定理（按 stmt_q），每个版本附一份证书。要补进包图 ADR。 4. 公理策略由验证方决定：证书列出所用的全部公理，验证时由使用者选择接受哪些。这对应 v0.2 的"公理足迹是类型的一部分"，再加上验证方的策略。 5. 零知识：证明本身不用公开，只证明"存在一个有效的证明"，可以保护知识产权。 **不该照搬的（这也是我们的差异化所在）：**信任基础。 - Nanoda 没有被证明是可靠的； - SP1 的电路要信任； - Groth16 需要可信设置（依赖 SP1 的那次仪式）； - 验证器是 TypeScript 写的。 而我们的方向是：检查器本身由可靠层证明（R-CIC 从 Lean 生成），链条末端是我们自己的 AIR/STARK，不需要可信设置。 一个可以马上用上的点：Nanoda 是一个独立实现的 Lean 内核。Assay 导入时，可以把同一份 Lean 导出同时交给 R-CIC 和 Nanoda 检查，作为对撞的第三方参照（Lean4Lean 也可以），这正是 GATE RULE 认可的"多基底一致"那类证据。 我的安排（省额度，只分发）： - 第 1、3、4 点给 ADR 车道：补进包图 ADR，并作为北极星路线里对外定位的参照； - Nanoda 当对撞参照这一条给 grok-import（Assay 导入器），作为一个测量项； - 记进 memory。

I also made a library called HTTPV (HTTP-Verified) HTTPV lets your server serve ZKLean certificates for each API endpoint, and lets your clients verify those certificates cheaply. Drop-in replacement for Bun.serve() Repo: ZeframLou/httpv

This means you can: - Cheaply check formal specs released by your dependencies - Ensure your formal proofs don't break on every release - Cheaply prove to someone your software is formally verified Repo: ZeframLou/zklean