A aplicação de algumas leis está sujeita a satisfação de uma ou mais condições que devem ser provadas para garantir a corretude da aplicação da lei. As obrigações de prova geradas ao longo do refinamento são exibidas na Janela de Obrigações de Prova.
Ao serem geradas, as obrigações são passados ao Provador de Teorema que deverá verificar a a obrigação de prova. Atualmente, temos apenas a verificação por um pequeno provador que fará análise sobre restrições sintáticas da Obrigação de prova. Assim, um status é associado a cada obrigação de prova. Tal status pode ser: (verdadeiro), (falso), (não determinado), (provado manualmente verdadeiro) e (provado manualmente falso).




Selecionando uma obrigação de prova, a linha de aplicação da lei que gerou tal obrigação é selecionada na janela Desenvolvimento.
Uma importante funcionalidade, fornecida pelo nosso pequeno Provador, é a de exibir as obrigações de prova na sua forma expandida, através das definições de suas funções sintáticas. Assim, para visualizarmos a versão expandida ou resumida de uma obrigação de prova, devemos selecionar a mesma e clicar com o botão direito do mouse para que um Popup Menu associado seja visualizado. Através desse Popup Menu, podemos acessar três funcionalidade importante: Prova Manual, Editar e Exibir.



A Prova Manual permite ao usuário definir o status para a obrigação de prova que o nosso provador não tem condições de determinar um valor. Como o próprio nome sugere, essas provas devem ter sido realizadas manualmente pelo usuário. Logo após ajustar o status de uma obrigação de prova, a janela de obrigação é atualizada. A ação de definir um status para uma obrigação de prova, também pode ser desfeito/refeito.
Outra importante funcionalidade é o fato de uma obrigação de prova, pode ser exibida no formato expandido ou resumido. O formato resumido é o formato padrão. O expandido, utiliza as definições das funções sintáticas de Circus, para exibir os correspondentes termos do predicado. Assim, apenas funções que possuem funções sintáticas possuem formato expandido para ser visualizado. Para selecionar tal formato, devemos ir no Popup Menu associado a janela de obrigação de prova e selecionar à seguinte opção: "Exibir->Expandido". Analogamente, também temos a opção: "Exibir->Resumido"



Após escolher o novo formato, a obrigação de prova é exibida no formato desejado. Essa ação também pode ser desfeita/refeita.



A funcionalidade de copiar o texto de uma obrigação de prova para utilizar em outra aplicação que não o CRefine é descrita em Copiar.