Full-stack verification is the new trend

There have been several recent announcements about formal verification of software and hardware, both using AI and for AI systems: Harmonic announced last week that they are using their agent Aristotle for scalable verification of both software and hardware. For example, in a C library for big-number arithmetic, it was able to fix bugs and prove that a faster version was equivalent to the original. The person whose work I particularly follow in this area is Satnam Singh, who has worked on hardware verification for several years. SF-Tensor announced that they were formalizing NVIDIA’s PTX language in Lean to prove the correctness of GPU kernels. SF-Tensor was founded by three brothers at the age of 19, after they had completed their BSc degrees at 16 while attending high school. &Truth came out of stealth, announcing plans to use Lean to prove the correctness of AI-generated software. Key people involved include Clark Barrett, known for his work on cvc5 and CSLib; Ilya Sergey, known…

Commenting on Bubbles has been removed. Why? If you want to talk about this post, write to the author, use the comments on their blog if it has them, or reply with a "RE:" post on your own blog. Suggestions? feedback@bubbles.town