Verifiable Keypoints

Passing verdicts from keypoint execution do not prove full correctness. A verifiable keypoint is modeled as a natural-language triple of precondition, bounded interaction, and expected postcondition. Each accepted keypoint is grounded into one or more verification units. Keypoint extraction requires constructibility, boundedness, and verifiability. A single keypoint can produce multiple verification units to cover boundary conditions.