NL-Verify is an educational software prototype designed to bridge the gap between natural language specifications and formal mathematical verification. Developed as a group project for the Programming Language Paradigm course, the system functions as a "Mini-Programming Language" that allows users—specifically Computer Science students—to write algorithmic specifications in Controlled Natural Language (e.g., "After the loop, total must equal sum of inputs"). The primary goal of NL-Verify is to demystify the "black box" of formal methods. Instead of requiring students to master complex mathematical notation (e.g., Hoare Logic triples) immediately, the system parses English input into an Abstract Syntax Tree (AST), translates it into semantic assertions, and utilizes the Z3 Theorem Prover to rigorously prove correctness using Axiomatic Semantics. Simultaneously, a Dynamic Test Generator creates concrete Python test vectors to validate the logic against runtime edge cases (such as division by zero). To enhance the learning experience, the system integrates an LLM-based refinement agent (Llama-3.2). This agent suggests improvements and corrects syntax errors or "slang" input, preventing system crashes and keeping the user focused on logical verification.