Show HN: A malleable and formally verified Web engine

Category: infrastructure

Tags: web-engine, formal-verification, rust, tla-plus, browser

Score: 6.3/10 (Innovation: 7, Technical: 8, Documentation: 6, Utility: 4)

formal-web is a Rust-based web engine prototype featuring a modular architecture where the JS engine, media backends, networking stack, IPC layer, and embedder are all swappable components. Its notable innovation is applying formal verification (TLA+ model checking against Rust implementation traces) to core algorithms from day one, alongside a design philosophy of leveraging OS-native facilities (Core Animation, AVFoundation, URLSession) for performance and minimal binary size. It's an ambitious research-grade project exploring verifiable, platform-adaptive browser engine design.

Target audience: browser engine researchers, systems programmers, formal methods practitioners

Repository: https://github.com/gterzian/formal-web · Rust · MIT · 33 stars

View on Hacker News