naso-llm：基于 Naso 形式化验证编译器的离线浏览器聊天机器人开源

naso-lang 在 GitHub 开源 naso-llm，一个可离线运行的浏览器聊天机器人，使用 SmolLM2-135M-Instruct，其 int8 权重量化由 Naso 形式化验证编译器生成，无需服务器、API key 或运行时构建。首次加载下载 269 MB 检查点后由 service worker 缓存，断网可用；2 核 CPU 上解码约 6.5 tokens/s。项目提供 17 项验证检查，包括与 Rust tokenizers 的 27/27 分词一致、基于 NumPy 独立实现的 forward 误差 max|Δ| 1.03e-5、106M 权重上 int8 误差界 |W−W′|≤scale/2 零违例、KV cache 与全序列 bit-identical 等。