Specification Engineering

This site provides an overview of CS 4501 Specification Engineering, an undergraduate course at the University of Virginia. The actual course content is hosted on UVA Canvas.

Agents write the code. Who decides what it should do?

AI agents can now write a working module in minutes, and increasingly they can write the proofs that it is correct too. But an agent builds what you asked for. If what you asked for is vague, incomplete, or wrong, you get well-tested, confident, wrong software.

As agents take over more of the coding, the skill that matters is saying precisely what a system must do and checking that what was built does it. Software engineers have long separated two questions: are we building the system right? (verification) and are we building the right system? (validation). Agents are getting good at the first, provided someone gives them a spec. This course teaches you to write that spec, show that it is the right one, and hold agents to it: to build the right system right. You will own the requirements and specifications; agents will write the code and proofs; a verifier will decide what gets accepted.

Industry is already moving this way. Spec-driven development tools such as Kiro and GitHub Spec Kit have agents work from written requirements and specifications instead of one-line prompts. This course goes two steps further: you will prove that code meets its specification, not just test it, and you will learn to show that the specification says what people actually meant.

A simple request

Here is a request you could implement in five minutes:

Rank the class roster by grade, highest first.

Here is a first attempt at saying precisely what that means, written in Verus, a verifier for Rust. The ensures clause is the specification: it states what must be true of the output out for every possible roster.


/// Rank the class roster by grade, highest first.
fn rank(roster: Vec<Student>) -> (out: Vec<Student>)
    ensures
        // highest grade first
        forall|i: int, j: int| 0 <= i < j < out.len() ==> out[i].grade >= out[j].grade,

See anything wrong with it? Take a minute before you read on. Think about what an implementation could return that meets this spec but that nobody would want. Think about the cases the one-line request never mentions.

Reveal: what this spec misses

Students can go missing. The spec says only that the output is in grade order. An implementation that returns an empty list meets it, for every roster, and Verus will happily prove so:
```
{
    Vec::new()   // verified!
}
```
Ties are left to chance. Ann and Bo both have a 92, and Ann is listed first in the roster. Should Ann come first in the ranking? Should ties be alphabetical? Or does nobody care? The request doesn't say, so the spec doesn't either. "Nobody cares" is a legitimate answer, but it should be a decision, not an accident.
What about a student with no grade yet? Ranked first, last, left out, or not allowed in the input at all? Every answer leads to a different spec.

Here is a spec that settles the first two questions (the third is still open):


/// The students in `s` whose grade is `g`, in the order they appear in `s`.
spec fn with_grade(s: Seq<Student>, g: u32) -> Seq<Student> {
    s.filter(|x: Student| x.grade == g)
}

/// Rank the class roster by grade, highest first.
fn rank(roster: Vec<Student>) -> (out: Vec<Student>)
    ensures
        // nobody lost, nobody added, nobody duplicated
        out@.to_multiset() == roster@.to_multiset(),
        // highest grade first
        forall|i: int, j: int| 0 <= i < j < out.len() ==> out[i].grade >= out[j].grade,
        // students with equal grades keep their roster order
        forall|g: u32| with_grade(out@, g) == with_grade(roster@, g),

None of these questions is hard. The point is that the request didn't answer them, and an agent asked to implement it won't ask them either: it will pick an answer silently.

What you will learn

The course is organized around three skills, in the order you will use them: write a spec, test it until you trust it, then hold code to it.

1. Write specifications

Requirements written in English are full of ambiguities and gaps, like the roster request. You will learn to find them and to turn requirements into precise, checkable specifications.

reading a professional requirements document critically, and rewriting requirements in a structured form (EARS) that exposes what is missing
logic for writing specifications: quantifiers, and mathematical types such as sequences, sets, multisets, and maps
contracts (preconditions and postconditions) and invariants, each traced back to the requirement it comes from

2. Show that a specification is the right one (validation)

A verifier can prove that code meets a spec, but nothing checks that the spec says what people meant. The first-attempt roster spec is a perfectly good spec; it just isn't the one anyone wanted. You will learn to produce evidence that a spec captures intent, evidence that convinces your team and not just the verifier.

Spec tests: concrete examples a spec must allow or forbid, checked by the verifier, one or more per requirement
Property-based testing of specs: running specs on thousands of generated inputs with tools such as verus-spec-check, and mutation testing to ask whether a spec can tell correct code from subtly broken code. The first-attempt roster spec can't tell a correct sort from one that drops the last student.
Probing specs for defects: specs that are contradictory (so they prove anything), impossible to implement, or too weak to determine the behavior that matters
Playing specs against each other: each member of your team writes a spec for the same requirement, and tools search for concrete cases where the specs disagree. Every disagreement is a question your team didn't know it had.
Asking stakeholders: turning those examples into concrete yes/no questions ("Ann and Bo both have 92, and Bo comes first. Acceptable?"), and using the answers to settle what the requirement means

3. Use specifications as guardrails for agents (verification)

Once you trust the spec, it becomes the bar that agent-written code must clear. A spec is mathematics, not code in any particular language, and you can enforce the same spec in different ways, each with a different guarantee:

test it: property-based tests check the spec on thousands of generated inputs,
model-check it: a bounded model checker such as Kani checks every input up to a size limit,
prove it: a verifier such as Verus proves it for every input, of every size.

Why does the difference matter? In 2015, researchers trying to formally verify TimSort, the sorting algorithm in the Java and Python standard libraries, found a bug that years of use and testing had missed: it shows up only on inputs far larger than anyone thought to test. You will learn what each kind of evidence guarantees, what it asks you to trust, and how to choose: test everything, and prove what matters most.

Along the way you will learn:

deductive verification in Verus: loop invariants, termination, ghost state, and diagnosing a proof that fails
proving small programs by hand, so you understand what you are asking agents to do
property-based testing and bounded model checking of code against a spec
directing agents to write code and proofs, and catching the ways they cut corners: weakening a spec, or assuming what they were asked to prove
stating exactly what has been proved, what has been assumed, and what is simply trusted

Learn by doing: a semester-long team project

The course is built around a team project on a real system with real requirements. Each team takes one application from NASA's open-source core Flight System (cFS), the flight software framework used on a number of NASA missions, and works from the requirements NASA published with it.

Real requirements have the same problems as the roster request. One cFS application must start a recovery procedure when a monitored condition "has failed for the table-defined consecutive number of times." Suppose the condition is checked three times and the results are Fail, then Error, then Fail. Is that two consecutive failures, or one? The requirements' own definition of "consecutive" says one. The C code says two. Which is right? In this course, the code does not get to decide. You do, with evidence.

Over the semester your team will:

audit your application's requirements and rewrite them in a precise, structured form,
formalize them as Verus specifications,
test and validate the specifications: run property-based tests, play teammates' specs against each other, probe for weaknesses, and resolve ambiguities by asking stakeholders concrete questions,
direct AI agents to write the code, test all of it against your specs, and have agents prove the critical core, and
present a case, defended orally, for what your team's verified application can and cannot be trusted to do.

Who should take this course

Prerequisites are CS 2120 (Discrete Mathematics and Theory 1) and CS 3140 (Software Development Essentials). No prior experience with Rust, Verus, or formal methods is assumed.

If you expect to spend your career working alongside AI agents and want to be the person who knows exactly what the software is supposed to do, and can show that it does, this course is for you.