# Daniel's Blog

## Advent of Code in Coq

Series status: Suspended

First post in 2020, last post in 2021

In this series, I apply the Coq proof assistant to formalize solutions to the puzzles to Advent of Code 2020. That is, I try to solve the problem, and formally prove that the solution is correct.

• Advent of Code in Coq - Day 1

3502 words, about 17 minutes to read.

The first puzzle of this year’s Advent of Code was quite simple, which gave me a thought: “Hey, this feels within reach for me to formally verify! . . .

• Advent of Code in Coq - Day 8

8572 words, about 41 minutes to read.

Huh? We’re on day 8? What happened to days 2 through 7? Well, for the most part, I didn’t think they were that interesting from the Coq point of view. . . .