h5i is an unified Rust framework for building, verifying, and hacking web apps.
A lesson from my PhD: we need both.
Find a counterexample in the running application.
Prove a stated rule for the modeled logic under explicit assumptions.
Axum-based framework with a separate kernel for application decisions and GPU support for suitable batch workloads.
Extract Rust logic, prove critical properties, and test proof sensitivity with mutations.
Explore any web app, replay HTTP requests, and turn confirmed findings into CI tests.
pub fn push_rule(event: &[u8], pattern: &[u8], display: &[u8], members: u64, minimum: u64, maximum: u64, power: u64, required: u64, enabled: bool, require_display: bool) -> u32 { if !enabled { return 0; } if power < required { return 0; } if members < minimum || members > maximum { return 0; } if !glob(event, pattern) { return 0; } // display-name check omitted 1 }
theorem insufficient_power_denies ... (h : power < required) : push_rule event pattern display members minimum maximum power required true requireDisplay = ok 0#u32 := by simp [push_rule, h]
#[kernel] pub unsafe fn push_batch(...) { let i = thread::index_1d() as usize; ... shared::push_rule(&events[row(i)], ...) }
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) } } } }
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 -- proof body omitted
$ h5i browser snapshot @e7 Order 1041 $ h5i websec replay req_3 \ --set query.id=1042 → req_4 · HTTP 200 $ h5i websec diff res_3 res_4 owner: Alice → Bob
NEXT