Hacker News with Generative AI: Formal Verification

Preventing conflicts in authoritative DNS config using formal verification (cloudflare.com)
Over the last year, Cloudflare has begun formally verifying the correctness of our internal DNS addressing behavior — the logic that determines which IP address a DNS query receives when it hits our authoritative nameserver.

DNS, Formal Verification, Security, Networking, Cloud Computing

64 points by rscho 10 days ago | 3 comments

Compiling C to Safe Rust, Formalized (arxiv.org)
The popularity of the Rust language continues to explode; yet, many critical codebases remain authored in C, and cannot be realistically rewritten by hand. Automatically translating C to Rust is thus an appealing course of action.

Rust, C, Programming Languages, Software Development, Formal Verification

291 points by love2read 28 days ago | 157 comments

The Hoare Cube (wordpress.com)
I wrote earlier this year about my attempt to understand the repercussions of toggling and when giving a semantics to Hoare triples.

Programming, Logic, Computer Science, Formal Verification

86 points by matt_d 44 days ago | 23 comments

Discharging Lean goals into SMT solvers (github.com/ufmg-smite)
This project is inspired by SMTCoq and aims to provide Lean tactics that discharge goals into SMT solvers. It is under active development and is currently in a beta phase. While it is ready for use, it is important to note that there are still some rough edges and ongoing improvements being made.

Software, Proof Assistants, Formal Verification

52 points by ndrwnaguib 57 days ago | 3 comments

Modelling the archetype of a message-passing bug with TLA+ (2022) (medium.com)
Two years ago, I tried to describe “the archetype of a message-passing bug”, using both a real-world example in Rust, as well as plain English.

Software Engineering, Programming Languages, Debugging, Rust, Formal Verification

30 points by surprisetalk 125 days ago | 4 comments

The Future of TLA+ [pdf] (azurewebsites.net)

Programming Languages, Software Engineering, Formal Verification

195 points by tkhattra 142 days ago | 105 comments

Streams, Calculational Proofs and Dafny (rdivyanshu.github.io)

Programming, Formal Verification, Software Engineering

35 points by misonic 164 days ago | 9 comments

Finding Simple Rewrite Rules for the JIT with Z3 (pypy.org)

Optimization, Programming Languages, Compiler Design, Formal Verification, Software Engineering

25 points by lukastyrychtr 183 days ago | 0 comments

Nondeterminism in Formal Specification (buttondown.email)