In this paper we address the problem of formal verification of websites by using declarative languages. In particular, we first define a model for websites which can intuitively be specified by using Maude. The model is defined to be well-suited for the formal verification of dynamic as well as static properties of the system.  A website is defined as a collection of web pages which are semantically connected in some way. External web pages (which are related pages not belonging to the website) are treated as the environment of the system. We also present the temporal logic which is used to specify properties of websites, and illustrate the kinds of properties that can be specified and verified by using the Maude model-checking tool. Finally, we have implemented a prototype by using the specification language Maude.