This upload contains the gzip archive of a QEMU Virtual Machine (qcow file) with an installed Ubuntu 22.04 x86_64 OS for testing the partially synthesised (i.e. generated from a Coq formalisation) and experimental Linux PC Speaker driver . More details on the project can be found in the Github repository. In order to start the VM, the archive needs to be unpacked (with gunzip) and QEMU needs to be installed. Also, the host system should have PulseAudio (which implies being Linux x86_64 itself). Then, the VM can be started with qemu-system-x86_64 -enable-kvm -m 8096 -drive file=CertPCSpkrVM.qcow,if=virtio -audiodev pa,id=snd0 -machine pcspk-audiodev=snd0 When the system is started, a terminal (which is linked as favourite) has to be started. The installation includes 3 directories in the folder ~/KernelModuleSynthesis of which "certpcspkr" is most important and the directory "certpcspkr" contains a README.md with more details. The other folders are a fork of CertiCoq and VeriFFI and used for compilation of the driver. First, the driver has to be built with: cd ~/KernelModuleSynthesis/certpcspkr_linux/src make CERTICOQ_PATH=../../CertiCoq_kmod VERIFFI_PATH=../../VeriFFI_contrib/ Then, the driver has to be installed (as administrator, the password is the username) sudo insmod certpcspkr.ko and the command "sudo dmesg" should show "Probing DONE" as one of the last lines. Then, executing beep -f 511 should produce a tone. Note that a frequency value beyond 511 makes the system currently freeze.