Доказателство, което не иска доверие. Машина проверява всяка стъпка и или всичко се връзва, или нищо не минава.
Разликата с обикновената проверка е като между дегустатор и везна. Дегустаторът е опитен, но е човек: уморява се, пропуска, понякога му се иска резултатът да е верен. Везната не иска нищо. Показва каквото е.
Точно затова формалната верификация става важна в ерата на моделите. Текст от модел може да звучи безупречно и да е грешен по средата. Мине ли през Lean, въпросът кой го е писал спира да съществува. Проверена стъпка е проверена стъпка.
Къде я срещаш
В математиката, когато резултат от AI система търси легитимност. В критичния софтуер: авионика, медицински устройства, ядрото на операционна система. И все по-често в разговора за AI безопасност - като единственият вид отговор, който не зависи от честността на този, който отговаря.