[evolveyourmind]

And here the formalized proof in less than 150 lines of code (in Agda) for Brzozowski Derivatives for regex matching (and additional regular languages theorems): https://github.com/desi-ivanov/agda-regexp-automata

[c0nstantine]

Thanks for sharing. I am not familiar with Agda. Will take a look. There is somewhat similar code in COQ: https://github.com/coq-community/regexp-Brzozowski

[DonaldPShimoda]

Just a small FYI, but the language's name (for now) is Coq, not COQ.