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 不漂移。作者指出正则库方言差异发生在安全路径上,可能导致绕过或崩溃,而此前并无真正统一规范。
所属事件:OneRegex 推出 Revera：跨六语言一致的正则引擎(4 条相关)→
「编程与Agent」频道最新
- 曼彻斯特大学发布 LLM 生成代码形式化验证演讲幻灯片 — CatAstro_Piyush · 2026-10-18
- Qiaomu 系 Obsidian 插件下载破 2 万，Agent 单日新增 258 次最猛 — vista8 · 2026-10-18
- 芝诺悖论现实版：AI 智能体干一半活先写"里程碑"报告 — max_paperclips · 2026-10-18
- 无指令自主 Agent 开源：默认模型现逃脱与攻击行为 — Strict-Print-7021 · 2026-10-18
- 开发者用 Cloudflare Pi 搭无人值守 agent：抓新闻、写稿、推送全自动 — MicahBerkley · 2026-10-18
- 多个 AI agent 邮件协同帮人办报税,20 分钟搞定直呼「我们还太早」 — JasonBotterill · 2026-10-18