Rocq-solid

A story about vericoding

Slides

• Rocq-solid — Reboot with AI PDF
• Stop testing, start proving — Typelevel Traverses Berlin PDF
• Stop testing, start proving — ScalaDays 2026 PDF

Links

• Talk abstract Reboot with AI
• rocq-solid GitHub
• Rocqducers: React components powered by verified reducers GitHub
• From Rocq to Metal: a pipeline for formally verified microcontroller firmware arXiv
• Encore!: a VM running Rocq-extracted code on microcontrollers GitHub
• encore-benchmarks: verified firmware workloads, from PIN codes to firmware updates GitHub
• rocq-extraction-scala: a Rocq plugin adding Scala 3 as an extraction target GitHub
• Boulodrome: an MCP server giving LLMs interactive access to Rocq proofs GitHub
• The Rocq Prover Web