Comment by jasongross

Model: https://github.com/theorem-labs/rocq-linux-process-semantics based on https://github.com/mit-plv/riscv-coq and Sail Binaries are split into sections with a Python script and imported into Rocq with rocq-read-file Workflow: https://theorem.dev/oss-verify/ , https://github.com/theorem-labs/oss-verify , https://github.com/theorem-labs/oss-verify-proofs