Build · Test · Verify

Secure Web Development
for Every Team

Build with agents. Red-team for bugs. Formally verify properties. Bring security into your workflow, from application logic to the running web app.

curl -fsSL https://h5i.dev/install.sh | sh -s -- --websec --test
[h5i] shop.example.test
Two scenes. In one, an agent drives a shop through h5i, replays an order request with another order id, gets a different customer's order back, and the shop's code shows the query that never checked the owner. In the other, a Rust kernel is written and h5i app extract translates it into Lean 4 definitions; the same rule is stated in Lean and proven; then the owner check is removed on purpose and the proof fails, so the mutant is caught.
The problem

Is the Web App Your AI Built Really Secure?

AI agents make it easy to ship code. Making sure that code is secure is still difficult. Web security needs two things, and they are two sides of one coin.

01

Find vulnerabilities →

Expert hackers are expensive. Red-teaming AI can go rogue.

Professional red teams are expensive, and AI agents can run out of control. Effective security testing needs both the right tools and enforceable limits on what agents can do, and a confirmed finding should run again in CI/CD so that a fixed bug stays fixed.

h5i recon
h5i browser
h5i websec
h5i test
h5i box 02

Prove correctness →

Proving correctness is hard.

Writing code is easier than proving it correct with a theorem prover like Lean 4. Ruling out bugs requires precise specifications, explicit assumptions, and proofs that the implementation satisfies them.

h5i app prove
h5i app mutate
Lean 4
01 / Red-teaming · any stack

Professional Red-Teaming
for Every Team

Use h5i with the web app you already have. Browser automation and direct HTTP control let your agent inspect application behavior and investigate security issues. No framework migration required. Use it only on applications you own or are authorized to test.

01 what the agent runs

  1. h5i browserExplore your app automatically

    Your agent can read pages, click, type, and extract data through compact snapshots.

  2. h5i websecTest HTTP requests directly

    Your agent can capture traffic, inspect and edit requests, and replay them.

  3. h5i boxSandboxed workflow

    Sandbox the entire AI agent workflow, with configurable network and filesystem limits.

  4. h5i testKeep it fixed

    Replay a confirmed finding as a flow in CI, so a fixed issue stays fixed.

02 what you review, in h5i ui

h5i console · checkout-idor +
←→↻localhost:8765/#/sandboxes/alice/sandboxlocalhost:8765/#/sessions/br_9f3k2a/historysitemapactionsfindingsreconabout
02 / Formal verification · Rust + Lean 4

Formal Verification
for Every Team

Build on Axum with a Rust application kernel that can be extracted into Lean 4. State the rules your app must preserve, then check proofs against that logic.

From Rust application logic to Lean-checked properties Aeneas extracts the Rust kernel of the bulletin board tutorial into Lean definitions. Developers supply theorems such as authorized, and the console's Apps view shows each theorem as proven, with the mutants its proof caught, over the latest verification receipt. 01 rust · the application kernel NORMAL lib.rs Cargo.toml rust · 153:16 toml · 1:1 149150151152153154155156157158159160161162 fn delete(user: u64, s: &Snapshot, id: u64) -> Outcome { match find_post(&s.posts, id) { None => Err(Error::NotFound), Some(p) => { if p.author == user || is_moderator(&s.moderators, user) { Ok((one(Write::DelPost(id)), Reply::Done)) } else { Err(Error::Forbidden) } } } } 123456789101112 [package] name = "board-kernel" description = "Tutorial 2: a verified bulletin board" edition = "2024" license = "Apache-2.0" version = "0.1.0" publish = false # Extracted to Lean by Charon + Aeneas. [dependencies] h5i-app-schema = { path = "…/crates/h5i-app-schema" } h5i-app-sql = { path = "…/crates/h5i-app-sql" } AENEAS extract 02 lean 4 · the proof you supply NORMAL proofs/Theorems.lean lean · 79:9 79808182 theorem authorized (a : Principal) (s : Snapshot) (c : Command) ws r (hinv : Inv (Snapshot.toSt s)) (h : transition a s c = .ok (.Ok (ws, r))) : ∀ w ∈ ws.val, allowed (Snapshot.toSt s) a.user.val w := by …
h5i console · apps+
←→↻localhost:8765/#/apps/board/theorems
h5i
Overview
Sessions
Sandboxes
Apps
Host
boardexamples/app/boardreceipt · just now
SpecTheorems 3Trust boundaryEvidence
theoremstatusmutantsaxioms
authorizedproven4 of 4 caughtstandard
inv_preservedproven5 of 5 caughtstandard
transition_totalproven3 of 3 caughtstandard
Explore the Rust tutorials How the proofs work
FAQ

Frequently asked questions

The short answers. The manual has the long ones.

What is h5i?
h5i is an open-source, agent-native workspace for secure web development. It provides browser and HTTP security testing, regression checks in CI, and configurable sandboxing. Its h5i-app framework, an Axum-based Rust framework, lets developers prove properties of their application logic in Lean 4.
Do I need to rewrite my app in Rust?
No. The browser, HTTP testing tools, and security regression tests work with existing web applications in any language. The application framework is optional, for teams that want to write and verify application logic in Rust. It ships as h5i-app, with its documentation and tutorials in the h5i repository.
Does a proof mean my entire app is secure?
No. A proof establishes a stated property of the verified logic under explicit assumptions. It does not establish that every route, authentication adapter, dependency, or deployment is correct. Testing and review are still needed at those boundaries.
Do I need to be a security expert to use h5i?
No. You tell your agent what to check in plain language, for example whether one user can read another user's orders. The agent explores the app in the browser, captures the requests behind each action, then edits and replays them to test the idea. Every request and response is recorded, so you, or a security reviewer later, can check the evidence behind a finding. Only test applications you own or are authorized to test.
Is h5i an automated vulnerability scanner?
No. h5i does not run a fixed list of checks against a URL and hand back a report. It gives your agent the tools a professional tester uses, and the agent decides what to try. Once a finding is confirmed, h5i test can replay it as a flow in CI, so a fixed issue stays fixed.
How does h5i compare with Playwright, Puppeteer, or Burp Suite?
Playwright and Puppeteer are the right choice when you want to script a browser by hand. Burp Suite is the right choice when an experienced tester wants the deepest workbench: an intercepting proxy, Scanner, Intruder, and extensions. h5i is for the case where your own AI agent runs the test end to end: one session drives the browser and records its traffic, and the agent edits, replays, and compares requests through a CLI built for it, inside a sandbox with a reviewable record. See the Burp Suite comparison.
Does h5i work on every website?
Yes. h5i's own engine handles content-heavy websites and common browser interactions. For a site that needs a full browser, h5i browser proxy runs Chromium through a per-session capture proxy, and websec, recon, replay, and audit work on that session the same way they do on a native one.
How is the agent contained?
The browser uses lightweight process isolation when available. To restrict the agent's other tools as well, sandbox the entire workflow and configure its network and filesystem policy; the options are supervised isolation, containers, and microVMs, and enforcement depends on the selected tier and host support. This limits what a misled agent can reach, but it does not prevent prompt injection: a tested application can still mislead the agent on a target you allowed.
Where do my credentials and data go?
Credentials stay out of the model. The agent references a named credential without reading its value, or a human takes control to log in, and the authenticated session continues without returning the password or cookie. h5i has no hosted service and stores its sessions locally. Browser traffic still goes to the websites you allow, and model traffic goes to your configured model provider.

Find Vulnerabilities.
Prove Correctness.

Start with security testing on your existing app, or explore verifiable Rust application logic. Open source, local-first, and designed to work with your own agent.

curl -fsSL https://h5i.dev/install.sh | sh -s -- --websec --test
Start your first session Explore the framework
h5i · demo film+
h5i.dev/demo ⤢