Qed: A Formally Verified Web Frontend Framework in Lean 4

Frontend bugs commonly emerge in user-facing environments, ranging from overlooked cases in reducers to render errors on empty lists and unexpected behaviors in production. While most frameworks provide a type checker and a test suite, Qed offers a more robust solution by leveraging Lean, a powerful proof assistant used by mathematicians to validate proofs.

With Qed, applications are written in Lean, and the same kernel that validates mathematical proofs ensures the integrity of frontend code. The command qed build transpiles Lean applications into standard JavaScript, free of dependencies such as Emscripten and WASM, resulting in a straightforward bundle of .mjs files ready for deployment. The verified proofs in Lean correspond directly to the JavaScript that executes in production, ensuring reliability and confidence in the codebase.

Key Features

• Guaranteed Safety: The architecture guarantees that update and view functions cannot crash because they are defined as total functions in Lean. Any errors, such as a missing case in a match statement or a non-terminating render, are caught as build errors rather than reaching the user.

• Invariants and Proofs: Developers can assert facts about their applications, allowing the Lean kernel to validate them. For instance, if using a counter, one can define an invariant to ensure that the count never goes negative:

  structure Model where  
    count : Int  
  deriving Repr, Inhabited  
  
  inductive Msg | increment | decrement | reset  
  

  With Qed, proving correctness is integrated within the build process, seamlessly checking that invariants hold across all possible states and transitions.

• Simple View Syntax: Views are constructed using JSX combined with Lean, allowing for intuitive syntax and easily manipulable components without complex hooks or state management systems. In Qed, the framework automatically decides how to manage updates, making rendering efficient and seamless.

• Verified Runtime: Verification extends to the runtime as well: Qed ensures that the generated JavaScript is consistent with the verified Lean code through an automated transpilation process that eliminates the potential for discrepancies. The only manual JavaScript consists of essential DOM interaction code, all other code is generated straight from Lean.

Core Functionality

1. Forms and JSON Handling: Define data structures and validation rules once, and Qed generates forms and JSON encoders/decoders from that single declaration, minimizing redundancy and maximizing type safety:

   schema Book where  
     id      : Codec.text.jsonOnly  
     title   : Codec.text.refine NonEmpty  
     year    : Codec.nat.refine Year  
   

2. Routing: The framework includes a router that ensures round-trip URL equivalence, with compile-time checks preventing invalid paths or routing errors from occurring.

3. Component Architecture: Simple and powerful component architecture supports state and view declaration together, allowing for clean and maintainable UI logic where verification of transitions is automatic.

Performance

Even with the rigorous proof obligations, Qed performs competitively, with the Lean engine adeptly managing which parts of the UI need updating—yielding efficient re-renders akin to other popular frameworks. The transpilation from Lean’s recursive functions to JavaScript ensures performance is not a trade-off for safety.

Getting Started

Installing Qed is straightforward, utilizing the Lean toolchain without heavy dependencies. The build process also simplifies development with features like:

curl -sSfL https://raw.githubusercontent.com/JacobAsmuth/qed/main/install.sh | sh
qed new myapp && cd myapp && qed dev      # → http://localhost:8000, live-reloading

Conclusion

Whether building complex applications or simple interfaces, Qed offers a unique approach to frontend development by combining formal verification with easy-to-use tools and frameworks derived from Lean. For more information and examples, it is recommended to explore the extensive documentation and example applications included in the repository.