Revera 开源:用 Lean 验证、六语言输出一致的 POSIX 正则引擎
jedisct1 · x · 2026-09-03
OneRegex 项目的 Revera 发布,一个 POSIX.1-2024 扩展正则表达式的净室实现:引擎只写一份,在 Lean 4 中对照形式模型验证,再生成 Go、Rust、Zig、C、C++、TypeScript 原生库,保证所有语言匹配结果、报错和资源边界完全一致。特点包括:有界内存与运行步数、契约 API 可查询单次匹配的堆/栈/步数上界(如 64KiB 输入下堆 1158 字节)、无 bindings 不漂移。作者指出正则库方言差异发生在安全路径上,可能导致绕过或崩溃,而此前并无真正统一规范。
所属事件:Revera 开源跨语言一致的 POSIX 正则引擎(4 条相关)→
「编程与Agent」频道最新
- 零代码调三项配置，Salesforce 企业 RAG 准确率从 62.5% 升至 92.5% — msrivastav13 · 2026-09-03
- 长程 agent 难靠蒸馏,数据合成难度天差地别 — JoshPurtell · 2026-09-03
- 如何让 LLM 可靠地把自然语言翻译成可执行的确定性逻辑 — OwlZealousideal4779 · 2026-09-03
- every 发布 Compound Writing 插件，把写作方法论装进 Claude Code — danshipper · 2026-09-03
- XBOW 详解规模化漏洞挖掘的隐性难题:如何判断两个发现是同一漏洞 — moyix · 2026-09-03
- fable-advisor：让 Fable 5.1 当架构师编排 GPT 实现 — daniel_mac8 · 2026-09-03