Hardware Verification in Lean?

Stream: general

[Riyaz Ahuja]

Just out of curiousity, are there any released/in-progress projects that use lean for hardware verification? Whether that means something like Rocq's Kami as a full hardware DSL in lean, or anything else, I just wanted to get a feel for if there's been any work done here or if there's low hanging fruit.

[Henrik Böving]

There's several people/organizations interested in or working on Verilog verification for Lean and at least one person on this Zulip wanted to do some work on a hardware DSL at some point.

[Shreyas Srinivas]

I have an in progress project. But it’s not like Kami. There are some folks interested in porting Clash. You can try porting Kami if you want to try that. It won’t be novel in a conceptual sense. Synchronous hardware verification has been done many times in various ITPs.

[Shreyas Srinivas]

It will definitely have some novelty in implementation.

[Shreyas Srinivas]

A shorter route might be to build kami on top of Veil.

[Shreyas Srinivas]

And then write your own extraction.

[Arthur Paulino]

I'm interested in this too

[Artur Lojewski]

Riyaz Ahuja said:

Just out of curiousity, are there any released/in-progress projects that use lean for hardware verification? Whether that means something like Rocq's Kami as a full hardware DSL in lean, or anything else, I just wanted to get a feel for if there's been any work done here or if there's low hanging fruit.

You could try to contact Mr. @Satnam Singh . He is starting to work at HarmonicMath exploring Aristotle applications for formal verification of hardware.

[Satnam Singh]

I start work on Monday. Let’s see what happens!

[Shreyas Srinivas]

Nice

Satnam Singh said:

I start work on Monday. Let’s see what happens!

I enjoyed your icfp talk. I hope I may DM you about collaborating on this sometime.