h5i-dev/h5i

h5i – Agent‑Native Web Security Workspace

What it is

• A command‑line workspace that lets you use AI agents to hunt for web‑app vulnerabilities and formally verify Rust web services.
• Two main modes:
  1. Red‑team (bug‑finding) – agents drive a headless browser, capture/modify HTTP traffic, crawl the site, and can be replayed in CI/CD.
  2. Formal verification – write the app with the h5i‑app Rust framework (Axum‑based), translate the code to Lean 4 via Aeneas, and prove properties such as authorization or data isolation.

Key components

Component	Role
h5i CLI	Unified interface for agents (browser, websec, recon, app commands).
Browser toolkit	Automates navigation, clicks, form filling, etc.
HTTP toolkit	Captures, mutates, replays requests; useful for regression testing.
Recon crawler	Finds hidden endpoints and parameters by crawling and JS analysis.
h5i‑app crate	Axum‑based Rust framework designed to be translatable to Lean 4.
Dashboard (h5i ui)	Local web UI showing agent sessions, traffic, and sandbox status.

Typical workflow

1. Install – one‑liner script adds the binary and optional plugins (websec, recon, test).
2. Red‑team – e.g.

   h5i browser open https://example.com
   h5i browser click @e3
   h5i websec requests            # view captured traffic
   h5i websec replay req_42 --set query.id=456
   h5i recon crawl --max-requests 200
   

   Agents can be run inside a sandbox with configurable FS/network limits, and the recorded flows can be stored and replayed in CI pipelines.
3. Build a verifiable app – e.g.

   h5i app new counter && cd counter   # scaffold a new project
   h5i app extract                     # turn Rust code into Lean 4
   h5i app prove                       # run Lean proof checker
   h5i app mutate                      # mutate code to see proof breakage
   

   The Rust crate is added as a dependency (h5i-app = "0.1.1") and supports features like HTTP and Postgres.
4. Monitor – launch the local UI with h5i ui to watch browser sessions and replay logs.

Why it matters

• Bridges AI‑driven security testing (rapid, agent‑controlled exploration) with formal methods (mathematical guarantees), a rare combination in the web‑security tooling space.
• Keeps the agent side lightweight (CLI commands) while offering a Rust‑first development path for provably‑secure services.

Getting started

• Install via the provided script or cargo install --path ..
• Add the binary as a skill (npx skills add h5i-dev/h5i) for agent runtimes.
• Read the full command reference in MANUAL.md or via man h5i.

License – Apache‑2.0.

---

All details are taken directly from the repository’s README.