This work presents VeGo (Verified Go), a deductive formal verification system that enables direct verification of standard Go source code and formalizes contract-precision checking (weakest precondition vs. strongest postcondition) using an explicit analogy to type inference.
Abstract
As formal methods are rapidly becoming accessible and practical due to AI coding agents, priority passes to assisting developers and students in generating specifications. Leveraging native HMX/SSA verifiers provide that support with rigorous mathematical guardrails. We present VeGo (Verified Go), a deductive formal verification system that enables direct verification of standard Go source code. VeGo incorporates Hoare-style contracts, loop invariants and integer variants, well-founded recursive measures, block-level scope invariants, and equational reasoning chains with primed variables directly as non-intrusive Go comments. We detail the language selection rationale justifying Go as an ideal balance over C, C++, Java, and Rust, strategically adopting Go's native multiple return values. We detail the tool architecture, exploiting the theoretical equivalence between Static Single Assignment (SSA) form and first-order functional programming to annotate code, desugar of clopen interval quantifiers, add Reynolds'skip statement, provide weakest precondition calculus, and native Hindley-Milner constraint inference, and verification condition resolution over the SSA form. We formalize contract-precision checking (weakest precondition vs. strongest postcondition) using an explicit analogy to type inference. Finally, we evaluate VeGo across educational textbooks and outline a roadmap for formal concurrency specifications using epistemic temporal logic.
FLEX is presented, a foundational Constrained Horn Clause (CHC) solver implemented in LEAN, that reduces the trusted base to the kernel alone, and allows using LEAN's entire proof ecosystem to verify low-level systems code, via three contributions.
J. Khan, Petros Markopoulos, Nicolás Lehmann et al.· 0 citations
Introductory computer science courses commonly use programming for instruction and assessment. This has several weaknesses because working code is not a reliable proxy for complete understanding. Elements of instruction – mathematics, a specific programming language, syntax, test-cases – all come together to conflate the boundaries and the specific purposes of these tools. We propose a correctness-first pedagogical framework for introductory computer science that separating semantic reasoning from syntactic implementation. The framework structures problem solving into four epistemic stages: blueprint specifications expressed as pre- and postconditions, natural-language operational steps that make program behaviour explicit, code implementation, and proof of correctness. Central to this approach is a natural-language intermediate layer that enables students to reason about computation independently of programming syntax, making formal correctness reasoning accessible in early coursework. We describe BOOP, a tool that implements this framework through lecture-integrated workflows and assignment support. BOOP is delivered via a web-based IDE and a VS Code extension, and provides automated checking of loop invariants and specifications. We report on a classroom deployment across two semesters (48 students). Qualitative analysis indicates earlier and more explicit engagement with correctness criteria, improved handling of edge cases, and increased willingness to reason beyond test inputs. Our results suggest that correctness-first instruction is both pedagogically feasible in introductory CS courses and necessary for realigning assessment practices with foundational computational thinking goals in the presence of increasingly capable code-generation tools.
Vaani Goenka, Aalok Thakkar· Annual Conference on Innovat...· 0 citations
This work presents a deductive verification framework based on a weighted assertion language and an intermediate verification language, whose weight domains are ordered structures with implication and coimplication, which let verification conditions express lower- and upper-bound obligations internally.
Emma Ahrens, Samuel Rode, Philipp Schröer et al.· 0 citations
Neuro-formal verification is introduced, which harnesses that automation for developers of mainstream programming languages and returns a Dafny proof of correctness or of a bug on 57% of the entries at 92% precision, and a CBMC counterexample for 63% of the buggy programs at 90% precision.
Developers use automated Move refactorings to improve the modular structure of source code and the assignment of responsibilities. Class- and method-level Move refactorings are automated in modern IDEs, but statement- and expression-level moves that adjust method boundaries remain largely unautomated. We formalize five variants of Move Statement refactoring as preconditions and steps grounded in four basic conditions covering data reachability, execution count, side effects, and syntactic constraints required for compilation, of which all but the side-effect condition are checked statically. Combined with existing techniques, this also yields finer-grained moves of expressions and partial expressions. We further refine the formalization iteratively against a real project, deriving twenty additional preconditions and steps that handle Java syntactic diversity in practice. We evaluate applicability and compilability on ten projects, and behavior preservation in a case study on one of them: Move Statement refactorings yield compilable code in 93.3-97.0% of applicable cases, and the case study shows that the observed behavioral changes stem from side-effect reordering left to developer judgment, not from defects in the statically checked conditions.
These results show that compiling procedural structure improves the reliability and efficiency of skill execution while retaining model judgment where it is needed, and shows that compiling procedural structure improves the reliability and efficiency of skill execution while retaining model judgment where it is needed.
Jayanaka L. Dantanarayana, Savini Kashmira, Lingjia Tang et al.· 0 citations