Hacker News with Generative AI: Formal Verification

Show HN: Formalizing Principia Mathematica using Lean (github.com/ndrwnaguib)
This project aims to formalize the first volume of Prof. Bertrand Russell’s Principia Mathematica using the Lean theorem prover.

Mathematics, Formal Verification, Theorem Proving, Logic

136 points by ndrwnaguib 14 hours ago | 29 comments

Spin: Formal verification of multi-threaded code (spinroot.com)
Spin is a widely used open-source software verification tool.

Software, Formal Verification, Multithreading, Open Source

7 points by fanf2 12 days ago | 2 comments

Clean, a formal verification DSL for ZK circuits in Lean4 (zksecurity.xyz)
We are really excited to share our initial steps towards building clean, an embedded DSL and formal verification framework for ZK circuits in Lean4.

Formal Verification, DSL, ZK Circuits, Lean4

77 points by vons 30 days ago | 5 comments

HoarePrompt: Structural Reasoning About Program Correctness in Natural Language (github.com/msv-lab)
HoarePrompt structurally reasons about program correctness in natural language using large language models (LLMs). Drawing inspiration from the strongest postcondition calculus, it employs a step-by-step process to generate natural language descriptions of reachable program states at various program points. By aligning formal semantics with informal requirements, HoarePrompt enables LLMs to detect bugs that violate natural language specifications.

Programming, Artificial Intelligence, Software Engineering, Formal Verification

6 points by mechtaev 31 days ago | 0 comments

Show HN: Formal Verification for Machine Learning Models Using Lean 4 (github.com/fraware)
Welcome to the Formal Verification of Machine Learning Models in Lean project. This repository provides a framework for specifying and proving properties—such as robustness, fairness, and interpretability—of machine learning models using Lean 4.

Machine Learning, Formal Verification, Lean 4, Software, GitHub

52 points by MADEinPARIS 34 days ago | 14 comments

Locks, leases, fencing tokens, FizzBee (surfingcomplexity.blog)
FizzBee is a new formal specification language, originally announced back in May of last year. FizzBee’s author, Jayaprabhakar (JP) Kadarkarai, reached out to me recently and asked me what I thought of it, so I decided to give it a go.

Programming Languages, Software Development, Formal Verification

57 points by azhenley 38 days ago | 9 comments

Coq-of-rust: Formal verification tool for Rust (github.com/formal-land)
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

Programming, Rust, Formal Verification, Software Development, Security

159 points by todsacerdoti 43 days ago | 42 comments

Software Foundations (cis.upenn.edu)
The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.

Software Foundations, Computer Science, Programming Languages, Formal Verification

6 points by Tomte 47 days ago | 0 comments

Formal Verification of Zero-Downtime Database Migration in PlusCal (biradarganesh25.github.io)
Formal verification can be used to analyze complex systems to ensure their correctness.

Formal Verification, Database Migration, Software, PlusCal

48 points by code_monk666 48 days ago | 6 comments

Comparing Two Verilog CPU Implementations Using EBMC (philipzucker.com)
About a year ago my friends and I built a 4bit cpu out of a kit from aliexpress. https://www.philipzucker.com/td4-4bit-cpu/ It’s a lot of fun. I also think the system is so simple that is is kind of a nice target for tinkering around with formal methods.

Hardware, Computer Architecture, Verilog, Formal Verification, CPU

5 points by PaulHoule 63 days ago | 0 comments

Five Kinds of Nondeterminism (buttondown.com)
No newsletter next week, I'm teaching a TLA+ workshop.

Computer Science, Programming, Theory, Logic, Formal Verification

135 points by BerislavLopac 66 days ago | 32 comments

Comparing Two Verilog CPU Implementations Using EBMC (philipzucker.com)
About a year ago my friends and I built a 4bit cpu out of a kit from aliexpress. https://www.philipzucker.com/td4-4bit-cpu/ It’s a lot of fun. I also think the system is so simple that is is kind of a nice target for tinkering around with formal methods.

Hardware, Formal Verification, Verilog

10 points by todsacerdoti 74 days ago | 1 comments

Nvidia Security Team: “What if we just stopped using C?” (2022) (adacore.com)
Today I want to share a great story about why many NVIDIA products are now running formally verified SPARK code. This blog post is in part a teaser for the case study that NVIDIA and AdaCore published today.

Software Security, Programming Languages, Formal Verification, Case Studies

306 points by transpute 75 days ago | 179 comments

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 109 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 126 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 143 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 156 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 223 days ago | 4 comments

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

Programming Languages, Software Engineering, Formal Verification

195 points by tkhattra 241 days ago | 105 comments

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

Programming, Formal Verification, Software Engineering

35 points by misonic 262 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 281 days ago | 0 comments

Nondeterminism in Formal Specification (buttondown.email)