proof*formal