Nesta palestra, apresentaremos uma especifica��o formal que desenvolvemos baseando-nos numa teoria psicol�gica. Tal especifica��o tem como objetivo permitir a constru��o de agentes de software fundamentados em teorias comportamentais, de modo que experimentos com tais agentes possam ser relacionados com teorias psicol�gicas reais. Explicaremos alguns detalhes da especifica��o, escrita com o m�todo Z. Ademais, apresentaremos os pontos fortes e fracos tanto da nossa abordagem, quanto do m�todo Z, que pudemos observar no decorrer do trabalho.