i5h/ icefish GitHub
Rust × Lean 4

The provable
web framework.

Build in Rust. Prove in Lean. Ship with confidence.

Get started View on GitHub

Built around axumLean 4 proofsPostgreSQL transactions

Interactive proof specimen

Follow the logic,
from source to theorem.

Hover a highlighted line to trace its counterpart. Break the code to see the guarantee disappear.

kernel.rsRust

            

            
            

              
Proofs.leanLean 4

              

            

          


          

            

            

              LEAN / CHECKED
              Every query stays inside its tenant.
              
The compiled statement cannot read or change rows belonging to another tenant.

            

            
THEOREMPg.compile_sound

          

        

        
Illustrative, precomputed examples based on proofs in the repository. No Lean process runs in your browser.

      


      

        
01 / GUARANTEES

        

          
What can I prove?

          
Prove what
matters.

          
Keep the decisive part of your app small and pure. i5h gives you the bridge from that Rust kernel to claims Lean can check.

        

        

          

            A / 01
            
            
Authorization

            
Show that every successful write satisfies your policy—for every actor, state, and command.

            WritesAuthorized transition policy
          

          

            B / 02
            
            
Tenant isolation

            
Prove compiled statements leave every other tenant’s rows unchanged.

            other_tenants db' = other_tenants db
          

          

            C / 03
            
            
State invariants

            
Show every accepted transition preserves the rules that keep your data valid.

            Inv s → transition s c = ok w → Inv (apply s w)
          

          

            D / 04
            
            
Confidentiality

            
Prove indistinguishable states produce the same visible outcome for a user.

            view u s₁ = view u s₂ → outcome₁ = outcome₂
          

        

      


      

        
02 / ARCHITECTURE

        

          
One path, end to end

          
Rust runs it.
Lean reasons about it.

          
The same pure kernel you ship is extracted into Lean. The shell handles HTTP and persistence without putting business decisions in handlers.

        

        

          

            01 · INPUT
            axum
            
Authenticate the actor and decode the command.

          

          
request

          

            02 · DECIDE
            Rust kernel
            
A pure transition returns writes and a reply.

            Aeneas ↗
          

          
writes

          

            03 · COMMIT
            PostgreSQL
            
Apply in one serializable, retryable transaction.

          

          

            PROOF LAYER
            Lean 4
            
Specs and theorems checked against the extracted kernel and storage path.

          

        

      


      

        
03 / TRUST

        

          

            
Clear by construction

            
Know exactly where
the proof ends.

            
i5h documents the boundary instead of hiding it. Your kernel and storage translation are proof territory; the runtime and external world remain explicit assumptions.

            Read the complete trust model →
          

          

            

               PROVEN IN LEAN
              
Pure kerneltransition · apply

              
Storage pathplan · compile · render

              
Selected codecstokens · JSON output

            

            
TRUST BOUNDARY

            

               ASSUMED / TESTED
              
PostgreSQL semantics

              
axum · tokio · hyper

              
Authentication facts

            

          

        

      


      

        
        

          
Start below the surface

          
Your first proven
Rust application.

          
Follow the calculator tutorial: define a pure kernel, run it behind axum, extract it, and check your first theorem.

          

            Open the tutorial →
            Clone the repository
          

        

        

          
terminal

          
$ git clone https://github.com/h5i-dev/i5h
$ cd i5h
$ cargo i5h-verify

extracting Rust kernels...       done
checking Lean projects...        done
checking trusted boundaries...    done

✓ all verification gates passed