Semi-formal reasoning occupies the middle ground between fully formal proof assistants (provably correct but impractical) and unstructured LLM judges (practical but unreliable).
Agentic setup enables exploration through tool calls but constrains execution. The agent navigates the codebase without running code.
Two patches claim to fix two-digit year formatting for years before 1000 CE. Unstructured reasoning assumes format() is Python's builtin. The certificate forces interprocedural tracing.
The certificate template enforces explicit evidence for every claim. You cannot submit a valid certificate without completing all three blocks.
The structured template creates demand for evidence, and the agent's tool calls supply it. Interprocedural reasoning emerges naturally from template requirements.
Semi-formal reasoning improves performance consistently across patch equivalence, fault localization, and code question answering.
Performance varies between curated challenging examples and real-world SWE-bench agent-generated patches.
The paper reports no latency measurements, no tokens-per-certificate data, and no cost comparison. This visualization shows hypothetical overhead based on structured output requirements.
Different use cases have different readiness levels. Code review tooling is more viable than automated RL reward signals.