h5i（发音为“high-five”）是一个面向 AI 智能体的 Web 安全测试工作空间，目标是通过两种互补的方式保障 Web 应用安全：用 AI 智能体发现漏洞，以及用形式化验证证明正确性。它强调“用智能体构建、用红队找 Bug、用形式化验证证明属性”。
用途 h5i 面向 Web 应用的安全工作，分为两大方向：
- 发现漏洞（红队测试）：为 AI 智能体提供统一的工具集，用于浏览器自动化、HTTP 流量操作和侦察，以测试现有 Web 应用中的漏洞、复现攻击，并在 CI/CD 中运行安全回归检查。
- 证明正确性（形式化验证）：使用 h5i-app（一个基于 Axum 的 Rust 框架）构建应用，并针对 Lean 4 进行验证，直接针对 Rust 实现证明授权、数据隔离和业务逻辑等属性。
主要能力 h5i 的智能体接口是一个 skill，由二进制文件携带。其红队测试能力包括：
- 浏览器自动化：导航应用、与表单交互、测试已认证的工作流。
- HTTP 安全测试：捕获、修改、重放和比较 HTTP 请求，以调查漏洞。
- 侦察：通过爬虫和 JavaScript 分析发现端点、参数和隐藏的攻击面。
- CI/CD：保存已确认的攻击流程，并在 CI/CD 中重放，以捕获安全回归。
- 沙箱化工作流：在具有可配置文件系统和网络限制的隔离环境中运行智能体。 h5i 可与任何 Web 服务配合使用，不论其使用何种框架，无需迁移到 h5i-app。
使用方式 打开你常用的智能体运行环境，并输入类似“Audit https://<your-target>.com with h5i.”的指令即可开始审计。智能体通过统一的 CLI 访问这些能力，你也可以通过仪表板监控其活动。仓库资料中还提到可安装 man 手册页并查看完整命令参考。
形式化验证与 h5i-app 红队测试通过测试发现 Bug；形式化验证则采取互补方法：证明指定属性对所有可能的输入和行为都成立。h5i-app 是一个基于 Axum 的 Rust Web 框架，使应用逻辑适合用 Lean 4 处理。可以用 Rust 编写 Web 应用，通过 Aeneas 将其转换为 Lean 4，然后证明授权、隔离、业务逻辑等多种属性。
适用场景
- 对现有 Web 应用进行红队安全测试、漏洞发现与攻击复现。
- 在 CI/CD 流水线中执行安全回归检查。
- 对采用 Rust 与 h5i-app 构建的应用进行授权、数据隔离和业务逻辑等形式化验证。
- 在需要隔离环境的场景下运行安全测试智能体。
限制与暂未提供的信息 仓库资料未提供具体的收费方式、价格、平台兼容性列表、性能效果或详细使用步骤；这些内容暂未提供。要了解完整命令与项目概况，可参考官方文档：官方网站提供项目概览与 Slides，MANUAL.md 或 man h5i 提供完整命令参考。项目采用 Apache License 2.0 许可。
