h5i (pronounced high-five) is a unified workspace for building secure web applications through two complementary approaches: finding bugs and proving correctness.
- Find Bugs (Red-Teaming): Equip your AI agents with headless browser automation and deep HTTP traffic control to explore apps, intercept requests, and uncover vulnerabilities inside a configurable sandbox. Perfect for bug bounties, penetration testing, and CI regressions.
- Prove Correctness (Formal Verification): Build your backend on
h5i-app(our Axum-based Rust framework) and use Lean 4 to formally verify your application logic, proving everything from tenant isolation and authorization to core business state invariants.
Build with agents. Red-team for bugs. Formally verify properties.
|
Red-teaming Browser + direct HTTP control |
Formal verification Rust + Lean 4 |
CI/CD Continuous security checks |
Sandboxed workflows Configurable limits + auditable sessions |
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 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 looks
# h5i skill show policy # or just read a pageA session combines one page state, cookie jar, network policy, and request record. Agents read pages, interact with elements, and extract structured data through one CLI:
h5i browser open https://docs.rs/ --allow docs.rs
h5i browser snapshot # page outline with @ref handles
h5i browser click @e3
h5i browser extract '{"titles": ["h2"]}' # structured extraction
h5i browser read https://docs.rs/ # one page, no persistent sessionThe native browser owns its network layer, so agents capture, inspect, edit,
replay, and compare HTTP traffic directly. Sites that need
full Chromium go through the same workbench via h5i browser proxy.
h5i browser open https://target.example --capture --allow target.example
h5i websec requests # list messages and IDs
h5i websec replay req_42 --set query.id=456 # edit and resend one
h5i websec diff res_42 res_43 # compare responses
h5i websec sequence flow.json # run a multi-step test
h5i recon endpoints --state confirmed # discovery, each row names its evidenceWe can replay confirmed attack flows in CI. See
examples/security-regression-ci for the
GitHub Actions template:
- uses: h5i-dev/h5i@v1
with:
target: http://localhost:3000
tests: .h5i-tests/testsSince AI agnets might run out of control and perform dangerous actions,
h5i offers an auditable sandbox, where h5i browser requests and
h5i browser audit show the full logs. For stronger isolation, a profile
in .h5i/env.toml picks a tier (workspace, process, supervised,
container, or microvm) and limits network egress and filesystem access.
h5i box create alpha --profile agent-claude # sandboxed git worktree
h5i box shell alpha # interactive confined session
h5i browser open https://docs.rs/ --in alpha # browser inside the box
h5i box propose alpha # reviewable snapshot
h5i box apply alpha # merge approved changes
h5i box rm alpha # discard itWatch it all from the host with h5i ui:
Red-teaming finds the bugs you did not anticipate. h5i-app is a Rust web
framework for proving, in Lean 4, the properties you can state.
[dependencies]
h5i-app = { version = "0.1", features = ["http", "postgres"] }- Write the logic as pure Rust functions and prove it in Lean 4 via Aeneas.
- Serve it with axum; handlers never touch the database.
- Prove that invariants hold for the rows loaded back from the database.
- Prove properties across requests, for every order in which clients' requests commit.
The kernel is one function that decides what a command does. This one, from the calculator tutorial, keeps one number per user:
pub fn transition(actor: &Principal, snap: &Snapshot, cmd: &Command) -> Result<(Option<Memory>, Reply), Error> {
match cmd {
Command::Set { value } => Ok((Some(Memory { user: actor.user, value: *value }), Reply::Value(*value))),
Command::Apply { op, arg } => {
let m = memory_of(&snap.memories, actor.user);
match compute(*op, m, *arg) {
Ok(v) => Ok((Some(Memory { user: actor.user, value: v }), Reply::Value(v))),
Err(e) => Err(e),
}
}
Command::Get => Ok((None, Reply::Value(memory_of(&snap.memories, actor.user)))),
}
}Aeneas translates it to Lean, where theorems about it are ordinary Lean:
theorem get_after (a : Principal) (s s' : Snapshot) (c : Command) (w : Option Memory) (v : U64)
(hroom : s.memories.length < Usize.max)
(ht : transition a s c = ok (.Ok (w, .Value v))) (hs : apply s w = ok s') :
transition a s' .Get = ok (.Ok (none, .Value v))See crates/h5i-app for the full kernel, the axum server around it, and the proof workflow, and TRUST.md for exactly what is proven and what is assumed.
- 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
What is h5i?
h5i is an open-source workspace for building secure web applications. The
h5i CLI is a red-teaming tool for AI agents. It drives a target through its
own lightweight Rust browser, or through a capture proxy in front of Chromium,
and lets the agent capture, inspect, replay, and compare the HTTP traffic from
policy-controlled, auditable, sandboxed sessions. h5i-app is a Rust web
framework whose application logic is proven in Lean 4.
Do I need h5i-app to red-team, or the h5i CLI to use h5i-app?
No. The CLI tests any running web application, whatever it is built on.
h5i-app is a crate you add to a Rust project and needs no h5i binary. They
meet when an agent builds an application on h5i-app inside an h5i sandbox and
red-teams it from the same box.
What does h5i-app actually prove?
Charon and Aeneas translate the kernel, the SQL planner and compiler, the JSON
writer, and the token codec to Lean, and every theorem is about that extracted
code. Proven: properties of transition, that compiled statements touch only
the tenant's rows, and that an invariant kept by accepted writes holds in every
database state and every snapshot loaded back, for every order in which
requests commit. Trusted, not proven: axum, PostgreSQL's statement semantics,
the HMAC key, the clock, and the translation tools. TRUST.md
has the full list.
Why use h5i instead of Playwright or Puppeteer?
Use Playwright or Puppeteer when maximum compatibility with complex websites is the priority. Use h5i when you want lower resource use, direct network controls, a complete session record, built-in HTTP testing tools, or a sandbox for the browser and agent.
Is h5i a replacement for Burp Suite?
Not for every use case. h5i is useful when an AI agent needs to browse an application and capture, edit, replay, and compare its HTTP traffic through one interface. Its native browser needs no proxy; the optional agent-browser lane creates and configures a per-session proxy and CA. Burp Suite remains better suited to mature manual workflows, automated scanning, extensions, and low-level protocol testing.
Does h5i work on every website?
No. h5i works best for content-heavy websites and common browser interactions.
For sites that need Chromium, run h5i browser proxy <url> and open the
printed command with agent-browser, or run Chromium inside an h5i sandbox.
Linux trusts the session CA. macOS passes --ignore-https-errors.
Is h5i sandboxed by default?
The browser uses lightweight process isolation when available. For stronger isolation, place the browser or the agent's entire workflow inside a supervised network sandbox, container, or microVM.
Can h5i prevent prompt injection?
No browser can reliably detect or prevent every prompt injection. h5i reduces the potential impact by treating page content as untrusted, restricting network and filesystem access, isolating credentials, and recording the resulting actions for review.
Can the agent see my passwords or cookies?
The agent can reference a named credential without reading its value, or a human can take control to log in. The authenticated session continues without returning the password or cookie to the model.
Does h5i keep my data local?
h5i has no hosted service and stores its sessions locally. Browser traffic still goes to websites you allow, and model traffic goes to your configured model provider.
Apache-2.0. See LICENSE.
