h5i v0.5.3

Install

One binary. h5i unifies web development, formal verification
with Lean 4, and red-teaming around a composable Rust framework.

Linux / macOS:

curl -L https://github.com/h5i-dev/h5i/releases/download/v0.5.3/h5i-v0.5.3-<TARGET>.tar.gz | tar -xz
sudo mv h5i /usr/local/bin/

Windows: download the .zip, extract h5i.exe, and add it to your PATH.

The browser

h5i browser open https://example.com
h5i browser snapshot
h5i browser requests     # what it asked for, and what was refused
h5i browser audit        # the whole session, afterwards

A session is Chromium, driven through
agent-browser
(npm install -g agent-browser), and captured at a proxy this
binary runs: every request is policy-checked and written down
before it moves.

The websec workbench

h5i-websec is a separate archive, and installing it is a
deliberate act:

curl -L https://github.com/h5i-dev/h5i/releases/download/v0.5.3/h5i-websec-v0.5.3-<TARGET>.tar.gz | tar -xz
h5i plugin install websec --from ./h5i-websec

It holds no privilege of its own: every verb runs the h5i browser
verbs a person would type, through the same policy, budget and
receipts.

The recon ledger

h5i-recon is the other plugin, and it arrives the same way:

curl -L https://github.com/h5i-dev/h5i/releases/download/v0.5.3/h5i-recon-v0.5.3-<TARGET>.tar.gz | tar -xz
h5i plugin install recon --from ./h5i-recon

It records what a target exposes, where each candidate came from,
and which stored message confirmed it. Discovery only: a URL read
out of a bundle stays a candidate until a request answers for it,
and nothing here is called a vulnerability.

Security regression tests

h5i-test replays repository-owned attack flows and hands their
evidence to repository-owned external oracles:

curl -L https://github.com/h5i-dev/h5i/releases/download/v0.5.3/h5i-test-v0.5.3-<TARGET>.tar.gz | tar -xz
h5i plugin install test --from ./h5i-test
h5i test .h5i-tests/tests --target http://localhost:3000

It writes JSON and JUnit. OpenAPI coverage is report-only unless
--min-coverage is explicitly supplied.

Every request it makes is checked against an allowlist — every
request and every redirect hop — and written to the log before any
bytes move. A request that is not in h5i browser requests did not
happen. What a box adds, with --in, is that the record gains a
witness outside the browser; on a bare host that part is not
claimed.

Available targets

Target	Platform
x86_64-unknown-linux-musl	Linux x86_64 (static, glibc-free)
aarch64-unknown-linux-musl	Linux arm64 (static, glibc-free)
aarch64-apple-darwin	macOS Apple Silicon (arm64)
x86_64-pc-windows-msvc	Windows x86_64

Intel Macs have no published build: Rosetta 2 translates x86_64 to
arm64, not the reverse, so the aarch64-apple-darwin archive will
not run there. Build from source instead:
cargo install --git https://github.com/h5i-dev/h5i

Each archive is accompanied by a .sha256 checksum file.

What's Changed

• h5i-app-schema: Lean lemmas for u32 columns by @Koukyosyumei in #769
• h5i-app-pg: verified TLS to PostgreSQL (feature tls) by @Koukyosyumei in #770
• bump h5i-app to 0.5.2 by @Koukyosyumei in #771
• App/range reads by @Koukyosyumei in #773
• add the download counter script by @Koukyosyumei in #772
• Add files via upload by @Koukyosyumei in #774
• h5i-app reads: range comparisons (>=, <) on integer columns by @Koukyosyumei in #775
• bump up to 0.5.3 by @Koukyosyumei in #776

Full Changelog: v0.5.2...v0.5.3