Back in 2023, I wrote [this comment](https://codeforces.me/blog/entry/113179?#comment-1007111):↵
> It's hard going. But it's worth giving a try. I'm working on [CoqCP](https://github.com/huynhtrankhanh/CoqCP), a repository of formalized CP proofs. No running programs yet, but there will be some. The repository is still in its early stages. I want the repository to be bigger and cover more CP problems. It would take me a lot of practice to be able to use the technology in contest, but I'm working to get there.↵
↵
And now, the project has a formal proof for the Koxia and Bracket problem. This demonstrates [CoqCP](https://github.com/huynhtrankhanh/CoqCP) has the ability to formally verify substantially complex algorithms.↵
↵
Throughout the years, I built substantial infrastructure to enable the verification of programs. I built a dual-target compiler that can compile code in my [internal imperative language](https://github.com/huynhtrankhanh/CoqCP/blob/main/docs/InternalImperativeLanguage.md) into both Rocq and C++. I wrote proofs for several competitive programming problems. And to be able to invest more time into the project, I turned CoqCP into my bachelor's thesis.↵
↵
Back then, the professor didn't want me to work on competitive programming problems because he thought that they were of little value. He told me to work on blockchain, but I still wanted to work on CoqCP for my thesis. So I designed a compromise. I made my dual-target compiler emit Solidity code, with the intention to totally remove Solidity functionality when the thesis is over. When I defended the thesis, I got 89/100. It wasn't the highest score, and the thesis committee didn't really understand what I was doing. But it was the culmination of the support I got from both the Lean and the Rocq communities and my determination to pursue the problem, even when formal verification was decried as completely infeasible for normal people.↵
↵
And then AI agents arrived. In October 2025, when I was working on creating training data for Project Numina, I realized that GPT-5 was able to generate correct proofs for mathematical problems in Lean. I created a pipeline to solve math problems by using Gemini Deep Think to solve the problem informally and GPT-5 to formalize the informal solution in Lean. And at that time, I realized that CoqCP could have a bright future ahead. And after that, I had to deal with some personal stuff.↵
↵
Recently, I resumed work on CoqCP, realizing that CoqCP is a valuable tool in the era of AI-generated code. I used GPT-6 to generate the code and proofs for several competitive programming problems, including a very hard problem, Koxia and Bracket. I also built the infrastructure for comparing proofs against a frozen specification, similar to the [Comparator](https://github.com/leanprover/comparator) tool by the Lean development team. I genuinely feel that the project has a lot of potential, not only in the realm of competitive programming, but also in the programming industry at large.↵
↵
There is one thing that I particularly like about my project. The very conservative and limited design of the internal imperative language ends up being a foundational pillar for CoqCP's success in this day and age. In the past, people chased very complex designs, allowed the source language to be existing programming languages like C and Rust with very complex—and in some cases, even poorly defined—semantics, in hopes that their frameworks could be of general use. Can their designs fare as well as my intentionally limited design?↵
↵
If you're interested, please consider joining the [Rocq community](https://rocq-prover.org/community), where you can discuss CoqCP and many other topics related to the beautiful field of formal verification. Remember that, even though AI is profoundly successful at formal verification, the field still stands on its own and has many distinctive characteristics that can't simply be subsumed into the banner of AI.
> It's hard going. But it's worth giving a try. I'm working on [CoqCP](https://github.com/huynhtrankhanh/CoqCP), a repository of formalized CP proofs. No running programs yet, but there will be some. The repository is still in its early stages. I want the repository to be bigger and cover more CP problems. It would take me a lot of practice to be able to use the technology in contest, but I'm working to get there.↵
↵
And now, the project has a formal proof for the Koxia and Bracket problem. This demonstrates [CoqCP](https://github.com/huynhtrankhanh/CoqCP) has the ability to formally verify substantially complex algorithms.↵
↵
Throughout the years, I built substantial infrastructure to enable the verification of programs. I built a dual-target compiler that can compile code in my [internal imperative language](https://github.com/huynhtrankhanh/CoqCP/blob/main/docs/InternalImperativeLanguage.md) into both Rocq and C++. I wrote proofs for several competitive programming problems. And to be able to invest more time into the project, I turned CoqCP into my bachelor's thesis.↵
↵
Back then, the professor didn't want me to work on competitive programming problems because he thought that they were of little value. He told me to work on blockchain, but I still wanted to work on CoqCP for my thesis. So I designed a compromise. I made my dual-target compiler emit Solidity code, with the intention to totally remove Solidity functionality when the thesis is over. When I defended the thesis, I got 89/100. It wasn't the highest score, and the thesis committee didn't really understand what I was doing. But it was the culmination of the support I got from both the Lean and the Rocq communities and my determination to pursue the problem, even when formal verification was decried as completely infeasible for normal people.↵
↵
And then AI agents arrived. In October 2025, when I was working on creating training data for Project Numina, I realized that GPT-5 was able to generate correct proofs for mathematical problems in Lean. I created a pipeline to solve math problems by using Gemini Deep Think to solve the problem informally and GPT-5 to formalize the informal solution in Lean. And at that time, I realized that CoqCP could have a bright future ahead. And after that, I had to deal with some personal stuff.↵
↵
Recently, I resumed work on CoqCP, realizing that CoqCP is a valuable tool in the era of AI-generated code. I used GPT-6 to generate the code and proofs for several competitive programming problems, including a very hard problem, Koxia and Bracket. I also built the infrastructure for comparing proofs against a frozen specification, similar to the [Comparator](https://github.com/leanprover/comparator) tool by the Lean development team. I genuinely feel that the project has a lot of potential, not only in the realm of competitive programming, but also in the programming industry at large.↵
↵
There is one thing that I particularly like about my project. The very conservative and limited design of the internal imperative language ends up being a foundational pillar for CoqCP's success in this day and age. In the past, people chased very complex designs, allowed the source language to be existing programming languages like C and Rust with very complex—and in some cases, even poorly defined—semantics, in hopes that their frameworks could be of general use. Can their designs fare as well as my intentionally limited design?↵
↵
If you're interested, please consider joining the [Rocq community](https://rocq-prover.org/community), where you can discuss CoqCP and many other topics related to the beautiful field of formal verification. Remember that, even though AI is profoundly successful at formal verification, the field still stands on its own and has many distinctive characteristics that can't simply be subsumed into the banner of AI.
