webAI has released TwIL-LM, a two-model family of formal-logic reasoners at 1.7B and 3B parameters. The 3B member, TwIL-LM3, is a merged fine-tune of SmolLM3-3B; the 1.7B member is a PEFT LoRA adapter for SmolLM2-1.7B-Instruct. Both target autoformalization: translating English into first-order logic and checking whether a conclusion follows from its premises. Both run locally, with a 1.06 GB quantized build for the 1.7B and a 1.78 GiB Q4_K_M GGUF for the 3B. webAI’s announcement frames the release around beating gpt-oss-120b on four of five formal-reasoning lanes. Both checkpoints ship under the webAI Non-Commercial License ver. 1.0; revenue-generating deployment requires a separate agreement. The 3B Q4_K_M GGUF runs on CPU or 4 GB of VRAM. webAI positions local execution for environments where data cannot leave the device. Applications include first-order logic translation, entailment classification, natural language to structured query, Lean formalization drafting, and a verifier layer. TwIL-LM3 was built in four stages: LoRA supervised fine-tuning, checkpoint fusion, WiSE-FT interpolation at λ = 0.25, and