Crux, a Precise Verifier for Rust and Other Languages | Hacker News Reader

Crux, a Precise Verifier for Rust and Other Languages

arxiv.org

100 pointsbelter13 comments

I find arxiv papers a bit scary, their page was more welcoming https://crux.galois.com

I agree. There's also a quick demo video which is very well done:

https://www.youtube.com/watch?v=dCNQFHjgotU

It doesn't answer some obvious questions I have though:

1. What are the limitations? Presumably it doesn't work with assembly, external C libraries etc. What about unsafe code? Traits? Heap allocation? Threads? Etc.

2. How is this different to other projects, e.g. Kani? Kani uses the CBMC checker which can use a variety of SMT solvers. IIRC symbol execution is a different approach to SMT solving but I can't remember the details. What practical impact does it have?

Seems like the paper is a result of more than work of 4 years, which I did not realize previously. Not a simple research, for sure.

What is scary about it? The monsters that will hunt you down once you click on "View PDF"?

PDFs are a crappy experience on most devices that are not made of paper.

Crappy ≠ scary.

Also, crappy only applies if you insist on using the wrong device for viewing them (pro tip: don't use a phone). Otherwise, the experience is superior.

Nah, on landscape displays too. I often find myself scrolling back up to get to the start of the right column of text.

You will need a display that can show the full page comfortably, that is true, but a 27inch monitor or a large iPad will do.

I'd prefer something more flexibel than PDF as well, but all alternatives compromise on quality and/or ease of use. There seems to be no market for good looking digital documents other than PDF.

I think it's because I am not used to reading academic papers, so I don't know how to read the paper or where to get started. Do I start from top to bottom? Those papers get quite big so I don't think that's the right approach, they also tend to get very meaty with the keywords so I end up reading the same sentence multiple times because I have to lookup every word or try to grasp the concept they are explaining. Maybe I should start with the abstract first? I don't know.

Top to bottom is usually the best way to go, especially read first abstract & introduction, but don't be afraid to skip sections if they seem unclear or you just don't understand what they are trying to tell you.

These days, you could put the paper into NotebookLM, and generate a podcast, that will generate something friendly, but might be partially wrong or skip over essential stuff.

NOTE: This is not libcrux the formally verified rust crypto library (and one of the underlying crypto primitives libraries for Firefox's NSS).

Galois often releases their tools for free. Their GitHub is here:

https://github.com/galoisinc/

How does this compare with FramaC and KLEE?

Reply on news.ycombinator.com