This artefact is provided to allow reproduction of the experimental measurement used for evaluation of the Rust package machine-check-avr 0.4.0 (https://crates.io/crates/machine-check-avr/0.4.0) which allows verification of machine-code systems based on AVR microcontrollers (currently, only ATmega328P). machine-check-avr provides a description of ATmega328P, which allows formal verification provided by the package machine-check (https://crates.io/crates/machine-check/0.3.0). 16 programs are provided in the artefact, ranging from trivial to variations of more complex programs. Their properties can be verified using a custom script. The results are output as semicolon-separated values which can be compared with reference measurements. The artefact consists of: - In the directory `projects`, projects for the Microchip Studio containing the program sources (assembly or C sources) and the project files from which the machine code can be built. The projects were built using Microchip Studio 7.0.2542, and the resulting Intel HEX files (`.hex`) containing the machine code of the respective programs are used for verification. - The script `measure.sh` is used to perform the measurements. The properties the programs should uphold are written in the script. - The file `reference.csv` contains the reference measurement.