[nickpsecurity]

You'd probably do it in the theorem prover extracting it to a language with a web framework or use a language with a web framework that are both easier to prove. Here's a few places to explore:

http://www.impredicative.com/ur/

https://wiki.haskell.org/Web/Frameworks

Note: You'd pick the purest of them probably.

Most work I've seen on web applications with formal focus used model checkers, though.

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.397....

https://www.iro.umontreal.ca/~sahraouh/papers/Forte2004.pdf