Features

Build, Verify, and Hack.

Explore h5i's unified workflow: build with composable Rust kernels, verify critical logic in Lean 4, and red-team the running app with browser, HTTP, and CI/CD security tools.

The security CLI works with any web stack, including apps that do not use h5i-app. Explore the framework → · Plugin installation →

01 / Web framework

Verifiable Web Framework

Build on h5i-app, a composable Axum-based Rust framework. Verify critical properties of application kernels in Lean 4, check proof sensitivity with mutations, and run shared kernel logic on GPUs for suitable batch workloads. Framework guide →

h5i app new

Composable Rust Kernels

Start an h5i-app project with application logic in pure Rust kernels. Handlers connect that logic to the web app while keeping the decisions ready for verification.
h5i app extract · prove

Formal Verification

Charon and Aeneas translate the Rust kernel into Lean 4. Prove authorization, tenant isolation, and state invariants across requests; the proof gate rejects sorry, native_decide, and stray axioms.
h5i app lint · mutate

Proof Validation

Lint that every mutating route takes an authenticated actor, then plant bugs in the kernel to check whether the proofs catch them. TRUST.md records the assumptions and trust boundary.
h5i-app-gpu · Rust-CUDA

GPU Acceleration

The Rust-CUDA backend runs shared Rust decision kernels on GPUs for suitable batch workloads. GPU report →
02 / Security testing

Red-Teaming & Security Testing

Explore any web application with browser automation and reconnaissance. Capture, edit, and replay HTTP traffic, then turn confirmed findings into repeatable CI/CD tests. Test only applications you own or are authorized to test.

02.1 / Recon plugin

Application reconnaissance

Build an endpoint inventory from the application and its traffic. Recon reference →

h5i recon extract · known · import

Find exposed endpoints

Extract URLs from HTML, JavaScript, JSON, and response headers. Include paths disclosed by robots.txt and sitemaps, or import inventories from other tools.
h5i recon crawl --max-requests 200 --rate 4

Crawl with explicit limits

Crawl under the browser session's identity and network policy, with request budgets, depth limits, and per-host rates. Resume interrupted jobs from recorded progress.
h5i recon triage · endpoints

Review endpoints with evidence

Separate unvisited candidates from observed and confirmed endpoints. Calibration identifies responses that differ from missing-page responses; recorded message IDs link observations to their evidence.
02.2 / Websec plugin

HTTP capture and editing

Inspect and test browser traffic for authorized web red teaming, pentesting, and CTFs. Web security guide →

h5i websec requests · show

Capture requests and responses

Inspect headers and bodies using stable message IDs. h5i owns its HTTP client, so no separate MITM proxy or CA setup is required.
h5i websec replay · diff

Edit, replay, and compare

Modify captured requests and replay them with the session's cookies and policy. Compare responses to see how the application behaved.
h5i websec match · sequence

Investigate multi-step flows

Match response content and combine requests into multi-step flows. Keep the requests and responses available for review before writing a regression test.
02.3 / Test plugin

Security Regression Testing

Turn a confirmed vulnerability into a versioned YAML test and replay it in CI/CD with an explicit verdict. Test reference →

h5i test .h5i-tests/tests/auth.yaml --target https://staging.example.com

Replay the attack flow

Run a saved test against staging or CI. Steps can use separate actors and cookie jars to check authorization across identities.
expect · oracle

State the security property

Check response status, headers, or body in the test, or use your own oracle for properties the built-in checks cannot express. An undecidable result is never treated as a pass.
03 / Execution & visibility

Sandboxing & Audit

Run agents inside explicit filesystem and network limits, then review browser traffic, policy decisions, and proposed changes in the local dashboard.

03.1 / Sandbox

Restrict the agent's access

Sandbox the entire red-teaming workflow to constrain tools. Policy guide →

h5i box . --profile <profile>

Isolate the workflow

Place the agent, code, dependencies, development server, and browser in one disposable environment, including a repository or pull request. Choose process, supervised, container, or microVM isolation according to host support.
.h5i/env.toml · h5i box probe

Set network and filesystem limits

Allow the destinations and files needed for the engagement. Enforcement depends on the selected tier and policy; an unrestricted workspace is not a sandbox.
h5i box secrets · h5i browser type --secret

Keep credentials outside the agent

Model and service credentials can remain on the host and be inserted into approved requests. The agent can use named browser credentials without reading their values.
h5i box --pr 1234 · h5i box cache refresh

Disposable test environments

Run a repository or pull request in an isolated workspace and reuse dependencies through read-only caches. PR review guide · Cache reference
03.2 / Audit and dashboard

Review what the agent did

Review actions and network activity, including blocked requests. The dashboard brings active sessions, isolation settings, and resource usage into one view.

h5i browser audit · requests

Session records

Review browser commands, allowed and denied requests, human takeovers, and session endings. A browser crash is recorded rather than silently replaced with a new session.
h5i ui

Independent observations

Host records remain outside the sandbox and distinguish boundary observations from browser reports. Watch active sessions and take over sensitive steps. Browser controls →
h5i box export <name> --out ./review

Reviewable output

Export a proposed patch, report, and execution receipt for review before applying changes. Audit guide →
h5i box view · h5i ui

Human review

Watch browser sessions and take over sensitive steps. Browser controls · Console
View the dashboard example
04 / Integrations

Works with Your Existing Tools

Use h5i from coding agents and CI/CD, and test web applications built with any framework.

h5i skill install

CLI for coding agents

Any agent that can run CLI tools can use h5i. Install the bundled skill for its command reference. Agent setup →
h5i browser · recon · websec

Existing web frameworks

Red-team apps built with any web stack. Browser, recon, and HTTP testing do not require a migration to h5i-app. Security testing guide →
h5i test .h5i-tests/tests/auth.yaml --target https://staging.example.com

CI/CD pipelines

Commit security tests alongside application code and replay them against staging to catch regressions. Review proposed changes from a disposable PR workspace.
FAQ

Frequently asked questions

How do I start with h5i-app?
Add h5i-app to a Rust project with cargo add h5i-app, or run h5i app new to create a project. Extract the application kernel to Lean 4 with h5i app extract and check proofs with h5i app prove.
Can I red-team an app built with another framework?
Yes. The browser, recon, HTTP testing, and security regression tools work with existing web applications in any stack. You do not need to adopt h5i-app.
Which security tools are optional plugins?
The browser is part of the h5i CLI. Recon, websec, and test are optional plugins; the installer accepts --recon, --websec, and --test to include them.
Does a Lean proof cover the entire app?
A proof establishes a stated property of the extracted kernel logic under explicit assumptions. Routes, authentication adapters, dependencies, deployments, and GPU execution still need testing and review.

Build, Verify & Hack

Start with the Rust web framework, or use the unified CLI to red-team any web application and replay security tests in CI/CD. Local-first, open source, Apache 2.0.

Rust web framework

cargo add h5i-app

Unified CLI and security plugins

curl -fsSL https://h5i.dev/install.sh | sh -s -- --websec --recon --test
View on GitHub Read the manual Explore the framework