Foreword

Software correctness is a cornerstone of reliable computing systems. As humanity invents and develops more sophisticated and immersive technologies, the demand for resilient software that behaves exactly as intended has become increasingly critical. We have always had systems that must never fail because their real-world side effects are irreversible by nature. For example, nuclear power plant control software should never drain coolant from a reactor, and cars must never deploy airbags at highway speeds when no collision occurred.

The Inference project started in January 2023 to address the challenges that this new era of computing brings. With the advent of blockchain and cryptographic protocols, quantum computing, AI-managed systems, and robotics, the need for software that is provably correct and secure has never been more pressing. No one wants a household robot to decide to iron clothes that are currently being worn by someone. Likewise, smart contract exploits do more than just drain funds, they hinder the evolution of financial systems.

Traditional testing and debugging methods, while useful, often fall short of providing absolute guarantees about program behavior. Formal Verification (FV), despite being one of the most advanced and reliable techniques for ensuring the correctness of algorithm implementations, has for decades been underrepresented and used primarily in aerospace, military, and other safety-critical industries.

Inference aims to bring Formal Verification into the software engineering mainstream.