Learning Latent Specifications from Structural Peers

Evaluating software correctness, from testing to formal verification, requires validating a program against a complete set of specifications, yet many codebases lack complete descriptions of their intended behavior. General properties such as memory safety rule out important classes of errors without application-specific knowledge, but functional errors can only be detected against application-specific constraints. Inferring those constraints from the code alone enshrines existing bugs, and documentation and requirements leave most functional contracts unstated. We propose a neuro-symbolic approach to infer latent specifications: constraints on intended behavior that are not documented but can be recovered by reconciling multiple sources of evidence. Our central hypothesis is that structurally related implementations within a codebase are evidence of shared invariants. Symbolic program analysis identifies groups of such structural peers and LLM agents then reconcile evidence from the peers, available documentation, and domain knowledge to infer candidate specifications and to decide whether differences between implementations are legitimate variation or deviations from intent (i.e. bugs). We evaluate the specifications our approach infers and assess their correctness using bug-detection as a proxy task. On a fixed checkout of wolfSSH containing 487 bugs and 5 CVEs, it achieves a recall of 5/5 of the CVEs and 72.9% on bugs subsequently fixed upstream, compared with 4/5 CVEs and 57.9% recall of the bugs for an unstructured LLM baseline given the same code scope.