Introduction

Duvet is a tool that establishes a bidirectional link between implementation and specification. This practice is called requirements traceability, which is defined as:

the ability to describe and follow the life of a requirement in both a forwards and backwards direction (i.e., from its origins, through its development and specification, to its subsequent deployment and use, and through periods of ongoing refinement and iteration in any of these phases)

Quick Start

Before getting started, Duvet requires a rust toolchain.

1. Install command

   $ cargo install duvet --locked
   

2. Initialize repository

   In this example, we are using Rust. However, Duvet can be used with any language.

   $ duvet init --lang-rust --specification https://www.rfc-editor.org/rfc/rfc2324
   

3. Add a implementation comment in the project

   // src/lib.rs
   
   //= https://www.rfc-editor.org/rfc/rfc2324#section-2.1.1
   //# A coffee pot server MUST accept both the BREW and POST method
   //# equivalently.

4. Generate a report

   $ duvet report
   

Configuration

Configuration files are written in the TOML format. The following is a quick overview of all settings:

# Specifies the version of the config
'$schema' = "https://awslabs.github.io/duvet/config/v0.4.json"

[[source]]
pattern = "src/**/*.rs" # Lists all of the source files to scan

[[source]]
pattern = "test/**/*.rs"
type = "test"            # Sets the default annotation type

[[source]]
pattern = "src/**/*.py"
type = "implementation"
# Sets the comment style for this group 
comment-style = { meta = "##=", content = "##%" }

[[source]]
pattern = "packages/other-repo/**/*.rs"
# Overrides the global blob-link for this source pattern
blob-link = "https://github.com/awslabs/other-repo/blob/main"

# Defines a required specification
[[specification]]
source = "https://www.rfc-editor.org/rfc/rfc2324" # URL to the specification

[[specification]]
source = "https://www.rfc-editor.org/rfc/rfc9000" # URL to the specification
format = "ietf"                                   # Specifies the format

[[specification]]
source = "my-specification.md" # Sets the local path to a specification

# Loads additional requirement files. By default it includes:
# * ".duvet/requirements/**/*.toml",
# * ".duvet/todos/**/*.toml",
# * ".duvet/exceptions/**/*.toml",
[[requirement]]
pattern = ".duvet/implications/**/*.toml"

[report.html]
enabled = true                                           # Enables the HTML report
path = ".duvet/reports/report.html"                      # Sets the path to the report output
issue-link = "https://github.com/awslabs/duvet/issues"   # Configures issue creation links
blob-link = "https://github.com/awslabs/duvet/blob/main" # Configures source file links

[report.json]
enabled = true                      # Enables the JSON report
path = ".duvet/reports/report.html" # Sets the path to the report output

[report.snapshot]
enabled = true               # Enables the snapshot report
path = ".duvet/snapshot.txt" # Sets the path to the report output

Specifications

Duvet currently supports two specification formats: IETF and Markdown. Specifications using either of these formats will be scanned for requirements using the RFC 2119 key words (e.g. MUST, SHOULD, MAY, etc.) and track completion of these requirements. If a specification does not use these key words, or has additional requirements, then requirement files can be provided in the configuration.

Annotations

Duvet scans source code for special comments containing references to specification text. By default, the comment style is the following:

//= https://www.rfc-editor.org/rfc/rfc2324#section-2.1.1
//# A coffee pot server MUST accept both the BREW and POST method
//# equivalently.

If the default comment style is not compatible with the language being used, it can be changed in the configuration with the comment-style field.

The default type of annotation is implementation, meaning the reference is implementing the cited text. The type of annotation can be changed with the type parameter. Duvet supports the following annotation types:

implementation

The source code is aiming to implement the cited text from the specification. This is the default annotation type.

test

The source code is aiming to test that the program implements the cited text correctly.

//= https://www.rfc-editor.org/rfc/rfc2324#section-2.1.1
//= type=test
//# A coffee pot server MUST accept both the BREW and POST method
//# equivalently.
#[test]
fn my_test() {
    // TODO
}

implication

The source code is both implementing and testing the cited text. This can be useful for requirements that are correct by construction. For example, let's say our specification says the following:

# Section

The function MUST return a 64-bit integer.

In a strongly-typed language, this requirement is being both implemented and tested by the compiler.

//= my-spec.md#section
//= type=implication
//# The function MUST return a 64-bit integer.
fn the_function() -> u64 {
    42
}

exception

The source code has defined an exception for a requirement and is explicitly choosing not to implement it. This could be for various reasons. For example, let's consider the following specification:

# Section

Implementations MAY panic on invalid arguments.

In our example here, we've chosen not to panic, but instead return an error. Annotations with the exception type can optionally provide a reason as to why the requirement is not being implemented.

//= my-spec.md#section
//= type=exception
//= reason=We prefer to return errors that can be handled by the caller.
//# Implementations MAY panic on invalid arguments.
fn the_function() -> Result<u64, Error> {
    // implementation here
}

todo

Some requirements may not be currently implemented but are on the product's roadmap. Such requirements can be annotated with the todo type to indicate this. Optionally, the annotation can provide a tracking issue for more context/updates.

//= my-spec.md#section
//= type=todo
//= tracking-issue=1234
//# Implementations SHOULD do this thing.

spec

The spec annotation type provides a way to annotate additional text in a specification that does not use the key words from RFC 2119, but is still considered as providing a requirement.

# Section

It's really important that implementations validate untrusted input.

//= my-spec.md#section
//= type=spec
//= level=MUST
//# It's really important that implementations validate untrusted input.

Additionally, Duvet also supports defining these requirements in toml:

[[spec]]
target = "my-spec.md#section"
level = "MUST"
quote = '''
It's really important that implementations validate untrusted input.
'''

Reports

Duvet provides a report command to provide insight into requirement coverage for a project. Each report has its own configuration.

HTML

The html report is enabled by default. It's rendered in a browser and makes it easy to explore all of the specifications being annotated and provides statuses for each requirement. Additionally, the specifications are highlighted with links back to the project's source code, which establishes a bidirectional link between source and specification.

Snapshot

The snapshot report provides a mechanism for projects to ensure requirement coverage does not change without explicit approvals. It accomplishes this by writing a simple text file to .duvet/snapshot.txt that can be checked against a derived snapshot in the project's CI. If the snapshot stored in the repo doesn't match the derived snapshot, we know there was an unintentional change in requirement coverage and the CI job fails.

$ duvet report --ci
 EXIT: Some(1)
   Extracting requirements
    Extracted requirements from 1 specifications
     Scanning sources
      Scanned 1 sources
      Parsing annotations
       Parsed 1 annotations
      Loading specifications
       Loaded 1 specifications
      Mapping sections
       Mapped 1 sections
     Matching references
      Matched 1 references
      Sorting references
       Sorted 1 references
      Writing .duvet/snapshot.txt

 Differences detected in .duvet/snapshot.txt:

 @@ -1 +1,3 @@
  SPECIFICATION: [Section](my-spec.md)
 +  SECTION: [Section](#section)
 +    TEXT[implementation]: here is a spec

   × .duvet/snapshot.txt
   ╰─▶ Report snapshot does not match with CI mode enabled.

This is what is known as a "snapshot test". Note that in order for this to work, the snapshot.txt file needs to be checked in to the source code's version control system, which ensures that it always tracks the state of the code.

Query

Duvet's query command is a development-time tool that answers focused questions about the project's traceability state. Where report produces the full artifact for CI, query is a fast feedback loop for the work in progress.

Checks

Each question query answers is a check, selected with --check (short: -c). Multiple checks can be combined in one invocation:

$ duvet query --check implementation
$ duvet query -c implementation,test
$ duvet query -c implementation -c test

Annotations of type citation, implication, and exception count as implementation. todo annotations are tracked separately — a requirement covered only by todo annotations is reported as "TODO only" by the implementation check, not as implemented.

Scope filters

By default each check considers every annotation in the project. Two flags narrow the scope:

• --section <PATH[#SECTION]> (short: -s, repeatable, comma-separated): restrict to annotations targeting specific specification sections.
• --quote <TEXT> (short: -q, repeatable): restrict to annotations whose quoted text contains the given substring (case-insensitive).

$ duvet query -c implementation -s spec.md
$ duvet query -c implementation -s 'spec.md#section-1'
$ duvet query -c test -q 'MUST encrypt'
$ duvet query -c implementation,test -s spec.md -q 'header'

Coverage checks

The coverage and executed-coverage checks correlate test annotations with executed implementation annotations using a coverage report:

$ duvet query -c coverage \
    --coverage-report 'target/jacoco/*.xml' \
    --coverage-format jacoco-xml

Both flags are required for coverage checks. --coverage-report (short: -r) accepts a glob and may be repeated. --coverage-format (short: -f) currently supports jacoco-xml.

For each test annotation in scope, duvet determines which lines were executed during the run, finds the implementation annotations that cover those lines, and reports whether the test's claimed implementations were actually exercised.

Two-phase coverage model

Coverage tools that operate on bytecode (e.g., JaCoCo) cannot report on source constructs that produce no executable instructions: method signatures, interface declarations, fields without initializers, and so on. Walking forward from an annotation to the next executable line breaks down whenever such a construct sits between the annotation and the code it describes.

For Java sources, duvet uses a verified two-phase coverage model from the duvet-coverage crate:

1. Target resolution — locate the source construct the annotation refers to (the next non-annotation, non-whitespace line below it).
2. Execution propagation — given the set of executed lines from the coverage report, derive which non-executable lines (declarations, scope openers) are transitively executed by virtue of being in a scope where some other line ran.

The algorithms are formally specified in design/query/coverage-model-spec.md and proven correct with Verus. The properties cover absence of false positives, no cross-scope leakage, conservative handling of non-linear control flow (goto, break to label, etc.), and monotonicity under coverage refinement.

For source files without a language-specific classifier, the coverage check uses a verified degraded model: the annotation resolves to its target line and status is read directly from the coverage report at that line, with no propagation. This is lower-fidelity than the two-phase model — constructs invisible to the coverage tool (declarations, signatures) cannot be credited — but its properties are proven with the same Verus machinery. Run with --verbose (-v) to see which path each file is using:

$ duvet query -c coverage -r '**/*.xml' -f jacoco-xml --verbose
...
Coverage model: 12 file(s) language-aware (verified), 3 file(s) degraded — no classifier (verified)
  degraded (no classifier, verified): src/main/python/loader.py
  degraded (no classifier, verified): src/main/c/parser.c
  degraded (no classifier, verified): src/main/rust/lib.rs

Verbose output

--verbose (short: -v) shows passing checks in full detail (matched annotations, source slices) in addition to the failures that are always shown. Use it during development when you want to inspect the matched state, not just the diagnostic for what's missing.

Exit code

duvet query exits 0 when every requested check passes, and 1 otherwise. The command is suitable for git hooks or per-commit validation; for CI gates, prefer duvet report --ci, which uses the snapshot mechanism for stability across refactors.

Relationship to duvet report

query and report are complementary:

query is the right command for "have I annotated this requirement yet?" report is the right command for "is the project's traceability state still acceptable?"

init

Initializes a duvet project

Usage: duvet init [OPTIONS]

Options:
      --specification <SPECIFICATION>  Include the given specification in the configuration
      --lang-c                         Include rules for the C language
      --lang-go                        Include rules for the Go language
      --lang-java                      Include rules for the Java language
      --lang-javascript                Include rules for the JavaScript language
      --lang-proverif                  Include rules for the ProVerif language
      --lang-cryptoverif               Include rules for the CryptoVerif language
      --lang-python                    Include rules for the Python language
      --lang-typescript                Include rules for the TypeScript language
      --lang-ruby                      Include rules for the Ruby language
      --lang-rust                      Include rules for the Rust language
  -h, --help                           Print help

extract

Extracts requirements out of a specification

Usage: duvet extract [OPTIONS] <TARGET_PATH>

Arguments:
  <TARGET_PATH>  

Options:
  -f, --format <FORMAT>            [default: IETF]
  -e, --extension <EXTENSION>      [default: toml]
  -o, --out <OUT>                  [default: .]
      --config-path <CONFIG_PATH>  
  -h, --help                       Print help

report

Generates reports for the project

Usage: duvet report [OPTIONS]

Options:
      --config-path <CONFIG_PATH>                
      --lcov <LCOV>                              
      --json <JSON>                              
      --json-v2 <JSON_V2>                        
      --html <HTML>                              
      --require-citations [<REQUIRE_CITATIONS>]  [possible values: true, false]
      --require-tests [<REQUIRE_TESTS>]          [possible values: true, false]
      --ci [<CI>]                                [possible values: true, false]
      --blob-link <BLOB_LINK>                    
      --issue-link <ISSUE_LINK>                  
  -h, --help                                     Print help