webAI has developed a family of formal-logic models designed to translate English into first-order logic and verify conclusions from premises. The models come in two sizes, with 1.7 billion and 3 billion parameters, and can run on local hardware with minimal memory requirements. The models are available for non-commercial use, with the larger model requiring 4GB of VRAM or a CPU to operate. The release highlights the potential for these models to be used in autoformalization tasks, although it notes that the benchmark scores provided are from an unreleased checkpoint. This development could have implications for the field of artificial intelligence and its applications in areas such as natural language processing and automated reasoning.