Engineering notes on verifiable web applications, formal verification, and agent-driven security testing.
Why h5i-app puts a small Rust decision kernel between Axum handlers and storage, then translates that kernel to Lean 4 for proofs.
Failed proof attempts led to confirmed Rust OSS bugs: an unscoped delete, a playlist metadata leak, and unbounded policy expansion.
Compare Burp Suite, OWASP ZAP, Caido, and h5i by the investigation each supports: manual proxy work, scanning, agent tooling, and browser-to-HTTP testing.
Why an agent sandbox must include child processes and browsers, how isolation tiers differ, and what prompt injection can still reach.
A patch shows what changed, but reviewing agent work also needs commands, browser activity, network decisions, missing evidence, and a controlled export.