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 mutationscurl -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 installedThe 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 looksLet 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://<your-target>.com with h5i."
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.
While agents access these capabilities through a unified CLI, you can also monitor their activity through the dashboard:
h5i ui # Open the local dashboard
- 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
h5i is licensed under the Apache License 2.0. See LICENSE.