In this work we propose an architecture for the formal verification of protocols and distribued algoritms. This can be see as a more abstract layer over the ordinary process of formal verification, where we have just the specification of the protocol and properties to be verified, and the formal tool. Our goal is to simplifu the specification and formal verification of protocols and distributed algorithms through a dedicated environment. The core of the architecture is its input specification language (Lep), which provides domain-specific constructions for simplifying the specification of those systems. With LEP the specification of the protocol and the specification of the topology to be referred to protocol are given separetely. We feel that this division improves the legibility of both and allows the reuse of the specification of a topology among distinct protocols. Using this approach we try to offer a language whose specifications should be similar to the descriptions of the algorithms found on the didactic books. Moreover, in order to have the input and output of the architecture compatible, we also propose a way of processing the result of the formal verification tool. Then we could have the result on the abstract level of LEP.