h5i: The Agent-Native Web Security Workspace

h5i-dev · h5i

10 min read Original article ↗
Skip to content

Build · Test · Verify

Secure Web Development
for Every Team

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

curl -fsSL https://h5i.dev/install.sh | sh -s -- --websec --test

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.

01 / Red-teaming

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.

02 / Formal verification

Proving correctness is hard.

Writing code is easier than proving it correct. Ruling out bugs requires precise specifications, explicit assumptions, and proofs that the implementation satisfies them.

⟹ You need a loop: find vulnerabilities, prove correctness, repeat.

The loop: find vulnerabilities, prove correctness, repeat Two steps joined into a cycle. Red-teaming the running app finds vulnerabilities, proving correctness in Lean 4 rules them out, and the loop repeats with every change the AI ships. 01 / RED-TEAMING Find vulnerabilities drive the app, replay, compare 02 / FORMAL VERIFICATION Prove correctness state a rule, check its proof REPEAT with every change the AI ships

Security testing / 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.

Explore the agent benchmark results →

01 the agent, in its shell

>_agent@box: ~/shop-audit + 

$ h5i browser open https://shop.example.test \
    --capture --session checkout-idor    # keep every message
$ h5i browser snapshot        # the page as an outline
$ h5i browser click @e7       # drive it like a user

$ h5i websec requests --human # what the session sent
  #107 GET  /checkout?order=1041  200  2.1 kB
  #108 GET  /api/order/1041       200  1.4 kB
$ h5i websec show req_108 --raw
  GET /api/order/1041 HTTP/1.1
  host: shop.example.test
$ h5i websec replay req_108 --set path=/api/order/1042
  res_109  200  1.9 kB
$ h5i websec diff res_108 res_109 --human
  status : 200 → 200
  bytes  : 1412 → 1903 (+491)
  alike  : 0.712

# Optional: run the same session inside a container.
$ h5i box --isolation container --name sandbox
$ h5i browser open https://shop.example.test --in sandbox
$ ▌

02 you, in the console

h5i console · checkout-idor +

←→↻localhost:8765/#/sandboxes/alice/sandboxlocalhost:8765/#/sessions/br_9f3k2a/historysitemapactionsfindingsreconabout

3 live214 recorded 1 sandbox1 refused egress9 runsstrongest container

checkout-idor

br_9f3k2a waiting on you 6 refused

https://shop.example.test/checkout?order=1042 h5i-lightengine-claimedalicelive for 2m

host:shop status:4xx|refused verb:replay▌

showrefusederrorsreplaysslowshop.example.test

#verbmethodhostpath ↓statustimeinitiator
108replayGETshop.example.test/api/order/104120031msreplay
109replayGETshop.example.test/api/order/104220029msreplay
110clickPOSTshop.example.test/api/pay40288mssubresource
111replayGETshop.example.test/api/order/9001refused—replay
112—GETpx.example.invalid/t.jsrefused—subresource

5 of 128 fetches match6 refusedthe oldest are in h5i websec requests

▾https://shop.example.testnav904

▾/api134

▾/orderGET34

10421

/cartGET POST7

/loginnav2

▸/assets74

▸https://cdn.example.test35

▸https://auth.example.test3

▸https://px.example.invalid2

https://shop.example.test/api/order/1042

1 allowed

methodsGET
statuses200
parametersnone seen
last fetchreq_109

h5i websec requests --session checkout-idor --host shop.example.test h5i websec show req_109 --session checkout-idor

4 origins · 7 paths6 refused3 paths that answered only 404 are left off

14:02:11openhttps://shop.example.test/3 fetches1.2s

14:02:14snapshot41 refs40ms

14:02:19click@e7 “Checkout”6 fetches310ms

14:02:31replayreq_108 path=/api/order/10421 fetch29ms

14:02:33diffres_108 res_109alike 0.71212ms

14:02:40replayreq_108 path=/api/order/90010 fetches—refused before the wire: the policy allows only the two test tenants

14:02:52click@e21 “Pay now”4 fetches · 40288ms

7 of 12 actions5 older foldedthe whole timeline: h5i browser audit

1 open0 closed

f_01

Order lookup answers for another tenant’s order

alice · 2m ago

rests onreq_108res_108res_109

  • replaying req_108 with order=1042 answered 200 with a different tenant’s order: 1412 → 1903 bytes, alike 0.712
  • the same replay with order=9001 was refused before the wire, so the probe stayed inside the two test tenants

idorunconfirmedh5i websec finding list --session checkout-idor

all 37live 29found, never sent 6gone 2probes

statemethodendpointstatuslearned fromevidence
liveGETshop.example.test/api/order/{id}200historyreq_109
livePOSTshop.example.test/api/pay402historyreq_110
liveGETshop.example.test/api/cart200historyreq_93
foundGETshop.example.test/api/order/export?from&tolink in /checkoutnever sent
foundGETshop.example.test/admin/ordersrobots.txtnever sent
goneGETshop.example.test/api/v1/order404probereq_61

6 of 37 endpointsthe ledger: h5i recon endpoints --session checkout-idor

Engine-claimed: the request log is the engine’s own account of what it fetched. It is fail-closed, so a fetch that is not in it did not happen, but nothing outside the engine vouches for it.

statelive
engineh5i-light
identityalice
policya1f4c9e70b32
captureon: 128 messages stored, owner-only
controlthe agent

h5i browser status --session checkout-idor h5i browser audit --session checkout-idor

alice/sandbox

containerbrowserrefused

EvidenceBrowser

The egress allowlist refused 2 requests to px.example.invalid:443.

policy allows

files$WORK rw

egressallow 3

exitany tool

limitswall 1800s

pagein box

h5i browser open https://shop.example.test

host-observedexit 01.2s14:02:11

·

✓ 3

✓

96M

✓

h5i websec replay req_108 --set path=/api/order/1042

host-observedexit 029ms14:02:31

·

✓ 1

✓

·

·

h5i browser click @e21

host-observedexit 088ms14:02:52

·

2 refused

✓

·

2

3 of 9 runs2 refusedthe receipts: h5i box status sandbox

Explore your app automatically

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

Test HTTP requests directly

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

Sandboxed workflow

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

Application framework / 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 specifications and proofs such as the authorized theorem. Lean checks the proofs against the extracted logic, establishing that every write is authorized, that invariants are preserved, and that no command panics. RUST / APPLICATION KERNEL

board › kernel › src › lib.rs board › kernel › Cargo.toml 149150151152 153154155156 157158159160 161162 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) } } } } 1234 5678 9101112 [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" } The logic your app runs AENEAS extract LEAN 4 / VERIFICATION BoardKernel.lean EXTRACTED 465466467 468469470 def delete (user : U64) (s : Snapshot) (id : U64) : Result … := do let o ← find_post s.posts id match o with | none => ok (.Err .NotFound) | some p => if p.author = user then … Theorems.lean YOU SUPPLY 77787980 818283 /-- Every successful write is allowed. -/ 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 … The extracted logic, checked against your specifications PASS PROVEN PROPERTIES authorized every write passes the policy inv_preserved invariants survive every step transition_total no panic, no overflow Checked by Lean

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. The companion i5h framework lets developers prove properties of Rust application logic in Lean 4; integration as h5i-app is planned.

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 is available today in the separate i5h repository, with its own documentation and tutorials; its integration into h5i as h5i-app is planned.

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 maximum website compatibility is the priority. 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?

No. h5i works best for content-heavy websites and common browser interactions, but some browser APIs are not yet supported. For incompatible websites, you can run Chromium inside an h5i sandbox.

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