AI 资源库 · 已整理 3 项
查看与verification-gates相关的 AI 资讯、工具、Skill、工作流和开源项目。
jjdeng-hub/elenva · ELENVA Web —— pi coding agent 的 Web 工作台（个人控制台，自用优先，非 IDE 前端）
ELENVA Web 是 pi coding agent 的 Web 工作台，定位为 Agent 控制台而非 IDE 前端，重点解决多会话编排与可见性问题：可查看哪些会话在运行、哪些被中断或报错、token 与成本消耗、子代理运行状态，并支持危险动作审批、每轮改动快照与整轮回滚、计划模式、上下文压缩记录、技能归档、工作树并行试验、离线用量聚合与插件市场安装。项目为个人自用优先，源码公开（MIT），后端逻辑 fork 自 pi-web，与 pi 共用 ~/.pi/agent/ 数据目录。
trestoncuzzort/dawnr · An assistant built to be trusted by proof, not by sounding right: a small language model trained from random weights on one machine, running with nothing behind it, whose programs carry specifications checked by seven provers (Dafny, Verus, SPARK, Frama-C, Lean 4, Rocq, F*), each also refuting a sabotaged twin. It learns only from what was proved.
dawnr 是一个以“先证明、后采信”为核心原则的助手项目，用小型语言模型生成带规格说明的程序，再交由 Dafny、Verus、SPARK、Frama-C、Lean 4、Rocq、F* 七种独立证明器检查。材料记录了学生模型在给定规格时的证明通过率、七证明器一致性门槛、构造性反例（被篡改孪生程序）检验、规格与问题一致性的额外检查，以及在本地硬件上以量化方式运行的整体流程。仓库同时包含从零训练核心模型、用已验证数据微调开源权重、强化学习与门控反馈成新数据、个人记忆与适配器、检索/语音/视觉/工具调用等实验性模块，并声明各项进展与已知失败模式。
JdominguezEcommium/agentic-self-regulation-loop · 2026 AI Agent Loop v2.0: Autonomous Coding with Guardrails & Self-Healing
OuroLoop GateKeeper 是一个面向 AI 编程 Agent（如 Claude Code、Cursor、Aider、Codex）的控制框架，通过意图验证、上下文完整性、执行安全、输出验证和集成检查五道验证门，配合三层自反思机制与自主修复引擎，将 AI 编程 Agent 从无约束的代码生成转变为受控的协作流程。README 还描述了多语言响应式监控面板、OpenAI/Claude API 集成与回退机制，以及 MIT 许可。