dranov

9 ms·

1.
by dranov 2mo ago
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 mak
2.
by dranov 7mo ago
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...
3.
by dranov 7y ago
> 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 not covered by RustBelt. To clarify, we do have a work-i
4.
by dranov 8y ago
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 correctness proof anyway, so bootstrapping in the
5.
by dranov 8y ago
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 “in the logic” – essentially, an application of the
6.
by dranov 8y ago
> 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 the transactions. However, agreement on the
7.
by dranov 8y ago
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 first results and I'm currently extending tha
8.
by dranov 8y ago
> 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 disabilities and is widely used in schools for the blind&qu
9.
by dranov 8y ago
> 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. FStar [1] has dependent types, monadic effects, refineme
10.
by dranov 8y ago
The link is that both these policies hurt US tech companies. With that lens, there is no inconsistency.
11.
by dranov 8y ago
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 Graph API launched on April 21, 2010. I
12.
by dranov 8y ago
That sounds a lot like BitMessage. https://bitmessage.org/bitmessage.pdf