This looks very interesting (and I am interested) but the article seems like a stub. I can't really find any documentation or meaningful source there.

However, X86 Proved is a thing and this is a presentation from 2014 I found:

https://people.csail.mit.edu/jgross/personal-website/present...

Before I submitted it to Lobsters, I checked the "Source Code" part of the link, allowed a few scripts in NoScript, and got this page with .v files that at least looked like the source code:

https://x86proved.codeplex.com/SourceControl/latest#src/

I'm a guy that tracks and reports on progress in this specialty but not a trained specialist. I don't know Coq well enough to tell you if this is the source code to the CoqASM paper with the quick skim I did before work. I do know it has a bunch of .v files going into detail about x86 and some other things with some overlap in aspects I thought I read about in the older paper. Hence, the submission claiming it was probably the same thing.

While we're at it, here's some other links on this sort of thing all of you might enjoy:

http://www.cs.cornell.edu/talc/

https://project-everest.github.io/assets/vale2017.pdf

https://github.com/project-everest/vale

> I don't know Coq well enough to tell you if this is the source code to the CoqASM paper with the quick skim I did before work.

It is.

See also https://www.microsoft.com/en-us/research/publication/high-le... for details on the program logic (ie. "Hoare triples for x86").

The main paper for this project is Andrew Kennedy's 2013 paper "Coq: The world's best macro assembler?"

https://www.microsoft.com/en-us/research/publication/coq-wor...

src: https://lobste.rs/s/kewmce/x86_proved_coq_library_for_modell...