Harmonic co-founder Tudor Achim discusses formal verificationFormal verification uses precisely stated properties and logical methods to check whether a system or argument satisfies those properties. with MTS host Sophia Dew. He describes translating the behavior of software and hardware into mathematical models that can be checked by a proof system.
Achim contrasts proving a specified property with searching for individual bugsSecurity testing evaluates whether a system's protections hold under defined conditions and identifies weaknesses that need fixing.. He says verification can address classes of memory-safety errorsMemory safety prevents software from accessing memory in invalid ways, such as reading outside an allocated region or using data after its storage has been released., while noting that verified code can still be insecure because of configuration or other problems outside the proof.
The conversation considers correctness, scale, speed and cost, and why the appropriate level of assurance depends on the consequences of failureA risk assessment identifies ways something could cause harm and examines their likelihood and consequences under specified conditions.. Achim argues that verification is especially important for critical infrastructure as AI-assisted attacks become more capable. These are his assessments, not an independent demonstration that all security risks have been eliminated.
Watch on YouTube
