What is runtime verification?

What is runtime verification?

Runtime verification is a method that watches a program as it runs and checks its behavior against properties written in advance. A monitor reads events from the run, e.g. each function call, and reports whether a property holds. The field is also called runtime monitoring. Developers use the same term for running the software to check a change.

Martin Leucker and Christian Schallhart give a definition in a 2009 paper. Their definition covers techniques that check "whether a run of a system under scrutiny" satisfies or violates a given correctness property. Exhaustive formal verification differs, because it uses mathematical reasoning to check a property on every possible run of a program or its model. Runtime verification checks only the runs that happen.

The developer meaning belongs to the testing side of a split that standards already make. NIST's Secure Software Development Framework treats reviewing code (PW.7) and testing executable code (PW.8) as separate practices, and suggests running tests in a sandboxed environment. For teams that test AI-generated code, the report that a coding agent writes about its change is not a run of the change.

Which meanings does runtime verification have?

The term has three meanings in common use:

• Formal methods. Runtime verification checks a run against a correctness property written in a formal notation, e.g. a temporal logic that describes the order of events. The Linux kernel includes monitors of this kind, which compare a trace of kernel events with a reference model of expected behavior.
• Developer testing. Developers use the term for running the software after a change and comparing what it does with what it should do. The International Software Testing Qualifications Board (ISTQB) calls any testing that executes the item under test dynamic testing. This meaning is the dynamic side of static and dynamic analysis.
• Runtime security. Some application security vendors use a longer phrase, runtime software verification, for watching software as it runs for signs of tampering or attack.

The first two meanings share one idea, which is checking a real run against what the software should do. For code that a coding agent wrote, the developer meaning is the one that answers whether the change works.

Some vendors call a run "runtime validation" and keep "verification" for checks that do not run the code. This learning center uses "verification" for any check that produces evidence about software, including a run. The standard split between verification and validation is a separate question.

How does runtime verification work?

In the formal meaning, a monitor checks a run in four steps:

1. A developer writes a property, e.g. "every file the program opens is closed before it exits."
2. A tool instruments the program so that it emits an event at each step the property names, e.g. each open and close call.
3. The monitor reads the events in order, either during the run (online) or from a recorded log afterward (offline).
4. The monitor returns satisfied or violated, and many monitors return inconclusive while the run so far could still end either way. A separate reaction can log a violation or stop the program.

In the developer meaning, a test runner checks a change in four steps:

1. The test runner builds the changed code and starts it in a clean sandbox.
2. The test runner drives the software through a workflow, e.g. with a headless browser for a web app.
3. The test runner records what the software did, e.g. the exit code of each command.
4. The test runner compares each record with a test oracle, the source of the expected result.

This usually means running the whole app, not only its unit tests, which each run one piece of code on its own. A smoke test is the shortest form. It checks that the build starts and its basic functions work. An end-to-end test follows a whole user journey.

What is an example of runtime verification?

Here is an illustrative example. Acme Co. sells furniture online. A developer asks a coding agent to "Let customers edit their delivery address during checkout." The agent changes the checkout code, and its unit tests pass.

The developer then writes one property for a monitor. Changing the delivery address must not change the items in the cart.

A test runner checks the change in five steps:

1. The test runner starts the changed store in a sandbox with a fresh database.
2. A headless browser adds 2 items to the cart and opens checkout.
3. The browser sets the delivery address to "12 Elm Street" and continues.
4. The store emits an event for each action, and the monitor reads the events in order.
5. The monitor returns "violated" at the last event, because the cart went from 2 items to 0.

The recorded trace and the monitor look like this:

type               address         items
cart.add           none            1
cart.add           none            2
checkout.open      none            2
address.update     12 Elm Street   2
checkout.continue  12 Elm Street   0

// Property: changing the address must not change the cart's items.
function checkCart(events) {
  const i = events.findIndex((e) => e.type === "address.update");
  const after = events.slice(i + 1);
  const next = after.find((e) => e.type === "checkout.continue");
  if (i === -1 || !next) return "inconclusive";
  return next.items === events[i].items ? "satisfied" : "violated";
}

The address saved, but the cart emptied. The browser chose the inputs, and the monitor only read the events. Each unit test checked one function, and none checked the cart after an address change. This example is simplified. A real project would check more properties across more workflows, e.g. one for the order total.

What can a run show that reading cannot?

Reading code, by a person or a tool, predicts behavior from the source. A run records what the changed software did, e.g. the emptied cart above, even when the changed lines look correct. A separate comparison of reading and running code lists the bugs each one finds.

What are the limits of runtime verification?

Runtime verification has five main limits:

• Unobserved paths stay unchecked. A quiet result means only that the checks that ran found no violation. No findings is not the same as complete coverage, and a run with gaps does not establish that the whole app works.
• Some properties stay open. A property about what must happen later, e.g. "each order ships eventually," can stay inconclusive, because a later event could still satisfy it.
• A weak property can pass broken software. A monitor checks only the property it was given. If that property misses part of the request, the run reports success on broken code, which is a false pass.
• Results depend on the environment. A run on a machine with leftover data can pass or fail for reasons the change did not cause. Test isolation gives each run its own clean state.
• Watching a run has a cost. A monitor inside the program uses its memory and time, so monitor design aims to keep that overhead low.

How is runtime verification different from monitoring?

Production monitoring collects signals from running software, e.g. an error rate, and alerts a person when a signal crosses a threshold. Runtime verification checks a run against a stated property and reports whether that property held. The two overlap when a monitor ships with the software and checks runs in production. In formal methods papers, "runtime monitoring" means runtime verification, not production monitoring.

In the formal meaning, testing differs from both, because a test chooses its inputs. A runtime monitor chooses no inputs, so Leucker and Schallhart describe runtime verification as a form of "passive testing."

How does RunStory help with runtime verification?

Checking a change in the developer meaning takes a run of the changed software, and a coding agent's report is not a run. RunStory runs your software in a separate environment, tries relevant workflows, and checks the results. It sends reproducible failures to your coding agent and verifies the fix. It is in private alpha for CLIs and web apps.

Join the RunStory alpha →

FAQs

What is runtime testing?

Runtime testing is testing that runs the software and checks what it does, which the ISTQB calls dynamic testing. It matches the developer meaning of runtime verification, which checks a change by running it.

Is runtime verification a formal method?

Runtime verification is a formal method in its original meaning, because its monitors check runs against properties written in a formal notation. Unlike exhaustive formal verification, it checks only the runs it observes, not every possible run. The developer meaning uses the same name for dynamic testing of a change.

Does runtime verification replace unit tests?

Runtime verification does not replace unit tests, and unit tests do not replace it. A unit test runs one piece of code on its own. A run of the whole app checks how the pieces work together, e.g. whether checkout keeps the cart after an address change.

What does "no failures found" mean after a run?

A result of "no failures found" means that the checks that ran found no violation. No findings is not the same as complete coverage, because paths that no run took stay unchecked, and a weak property can pass broken software.