Viewing profile — dranov

Check out https://veil.dev/ There's a blog post with a demo at https://proofsandintuitions.net/2026/02/09/distributed-verif... It's still early days, but we're committed to making …

Cedar used to be written in Dafny, but AWS abandoned that implementation and rewrote it in Lean. https://aws.amazon.com/blogs/opensource/lean-into-verified-s...

> I looked a little into RustBelt; how would it have helped this `Pin` issue? I browsed [1] a bit and it seems like `Pin` would have to have been proven on its own in an ad-hoc way…

I might be mistaken, but my understanding is that it does not. You still need to trust the implementation of the logic. But if you don't trust that, you wouldn't trust the compiler…

CompCert doesn't do this, but CakeML, a verified compiler for a variant of ML bootstraps itself in the logic : > A unique feature of the CakeML compiler is that it is bootstrapped …

> Are you including Bitcoin script when you say consensus? Currently, no. Our model considers "consensus" to be agreement on the ordering of transactions. We don't yet interpret th…

I agree, and there are efforts to develop formally verified implementations of Nakamoto consensus (which I'm involved in). We've published a paper a year ago about our efforts and …

> I’d really appreciate [...] links to the work of similar initiatives Take a look at Quorum, a "programming language which is designed to be accessible to individuals with disabil…

> SAT solvers generally have poor support for constructive logic, the kind of logic used in theorem provers based on dependent types like Coq. Arguably, this is no longer the case.…

The link is that both these policies hurt US tech companies. With that lens, there is no inconsistency.

Apparently, v1.0 of the Facebook Graph API could access users' private messages via the 'read_mailbox' API request [1]. This was deprecated when v2.0 launched. " Version 1.0 of the…

That sounds a lot like BitMessage. https://bitmessage.org/bitmessage.pdf