BAIF: Verilib Launch

​Verilib

​In the past, you needed years and a team of mathematicians to formally verify that your code does exactly what it should and nothing more. Verilib is a set of tools that enable formal verification for real-world applications, allowing engineers to develop with confidence that their code is scientifically proven to be bug-free and secure. Our goal is to significantly reduce the human effort required for formal verification by leveraging LLMs and other emerging technologies, ultimately making the world a safer place.

We're excited to finally unveil what we've been working on! Come see the first public demo of Verilib - our open-source library for formally verified code that we think could genuinely change how we approach software reliability.

​What you'll see:

• ​Hands-on walkthrough of the tools (warts and all - this is early stage stuff)

• ​Interactive discussion about making formal verification actually practical for everyday developers

​The idea is simple but powerful - instead of just testing code and crossing our fingers, we can now prove mathematically that it works. What's changed is that AI has gotten good enough at both writing code and generating proofs that formal verification might finally be accessible beyond academic research labs.

​We're particularly excited about the potential for AI safety: rather than trying to make AI systems themselves more trustworthy, we can have them generate provably correct code that implements their capabilities.

​Come if you're curious about: Software reliability, AI safety, verification tools, or just want to see some genuinely novel tech. We're looking for feedback from people who might actually use this, so expect plenty of discussion about what works and what still needs fixing.