An experimentation activity in automated set-reasoning is reported. The methodology adopted is based on an equational re- engineering of ZF set theory within the ground formalism L× developed by Tarski and Givant. On top of a kernel axiomatization of map algebra we develop a layered formalization of basic set-theoretical concepts. A first-order theorem prover is exploited to obtain automated certification and validation of this layered architecture.
