Аннотация:В работе предложен метод верификации функциональных программ, основанный на автоматическом доказательстве теорем. Метод основан на применении дедуктивных таблиц, в которые добавляются утверждения о программе и её свойствах. Предложенный метод позволяет как показать выполнение свойств программы, заданных в форме постусловия и предусловия, так и эквивалентность функциональных программ. Предлагаемый метод верификации реализован в прототипной системе верификации программ на языке Лисп.