Benchmarks for h5i-app, a Rust framework whose kernel is extracted to Lean 4 and proved there.
| Benchmark | Question | Source | Results |
|---|---|---|---|
| Verification | How much real-world Rust can h5i-app prove? | prove/ |
benchmark.h5i.dev/prove |
| Performance | Is an h5i-app server as fast as Go, TypeScript or Python? | performance/ |
benchmark.h5i.dev/performance |
Apache-2.0. Ported code keeps its upstream license (nora: MIT).