The Agent-Native Web Security Workspace
h5i (pronounced high-five) is a workspace for securing web applications through two complementary approaches: finding vulnerabilities with AI agents and proving correctness with formal verification.
- Find Bugs (Red-Teaming): Give AI agents a unified toolkit for browser automation, HTTP traffic manipulation, and reconnaissance. Test existing web applications for vulnerabilities, reproduce attacks, and run security regression checks in CI/CD.
- Prove Correctness (Formal Verification): Build applications with
h5i-app, an Axum-based Rust framework designed for verification with Lean 4. Prove authorization, data isolation, and business logic properties directly against your Rust implementation.
Build with agents. Red-team for bugs. Formally verify properties.
# Find bugs in web applications
h5i browser open https://example.com # Open a website in the browser
h5i browser click @e3 # Interact with page elements
h5i websec requests # Inspect captured HTTP traffic
h5i websec replay req_42 --set query.id=456 # Modify and replay a request
h5i recon crawl --max-requests 200 # Crawl the application for attack surfaces
# Prove correctness of Rust application logic
h5i app new counter && cd counter # Create an h5i-app project
h5i app extract # Translate Rust logic into Lean 4
h5i app prove # Build and check formal proofs
h5i app mutate # Test proof sensitivity with mutations
1. Install
curl -fsSL https://h5i.dev/install.sh | sh -s -- --websec --recon --test # `websec`, `recon`, and `test` are optional plugins
# curl -fsSL https://raw.githubusercontent.com/h5i-dev/h5i/main/install.sh | sh # if you would rather not add a domain to the chain:
# cargo install --path . # build from source
# h5i plugin list # says what is installed
The agent-facing interface is a skill, and the binary carries it:
npx skills add h5i-dev/h5i # if you do not have the binary yet
# h5i skill install # writes it where your runtime looks
2. Find Bugs: Red-Team with Agents
Let AI agents explore, attack, and test web applications using h5i's integrated security toolkit.
h5iworks with any web services regardless of their framework, and no migration toh5i-appis required.
- Browser automation: Navigate applications, interact with forms, and test authenticated workflows.
- HTTP security testing: Capture, modify, replay, and compare HTTP requests to investigate vulnerabilities.
- Recon: Discover endpoints, parameters, and hidden attack surfaces through crawling and JavaScript analysis.
- CI/CD: Save confirmed attack flows and replay them in CI/CD to catch security regressions.
- Sandboxed workflow: Run agents in isolated environments with configurable filesystem and network restrictions.
Just open your favorite agent harness and say "Audit https://.com with h5i."
3. Prove Correctness: Build on h5i-app
h5i-app is an Axum-based Rust web framework that makes application logic amenable to Lean 4.
Red-teaming discovers bugs through testing. Formal verification takes a complementary approach: proving that specified properties hold for all possible inputs and behaviors.
[dependencies]
h5i-app = { version = "0.1.1", features = ["http", "postgres"] }
We can write web applications in Rust, translate them into Lean 4 via Aeneas, and prove various properties like authorization, isolation, business logics, and more.
4. Dashboard
While agents access these capabilities through a unified CLI, you can also monitor their activity through the dashboard:
h5i ui # Open the local dashboard
5. Documentation
- Official Website: project overview, Slides
- MANUAL.md /
man h5i: full command reference - CONTRIBUTING.md: we welcome contributions of any kind
curl -fsSL https://h5i.dev/man/man1/h5i.1 -o ~/.local/share/man/man1/h5i.1: install the man page
6. License
h5i is licensed under the Apache License 2.0. See LICENSE.