Последние новости

Ghidra + CBMC = Assembly Model Checker

Future of Programming

Ship Your Interpreter

HOL Light Tutorial

Creusot 0.14.0 release - Contracts for Rust, formally proved

Refinement E-Graphs

What TLA+ can and can't check

DogWood: Monitoring Policies using First Order Temporal Logic

Proof Without Sharing Source Code: SJV, SJP, and the Trust Boundary

What if you need to demonstrate properties of a software module without giving the other party its source code? This comes up in real projects: prop…

Can we have reachability properties in TLA⁺?

Lambda MicroEgg

I Built Formal Verification for Compiled Sekura JS Programs with SJV and Z3

Most developers trust this pipeline: source code ↓ compiler ↓ binary If the source looks correct and the tests pass, we usually assume the compiled…

A preview of the future Intel Architecture documentation

The changing role of finite-state model checking

Foundational Verification of Running-Time Bounds for Interactive Programs

Improving system safety with Temporal Logic of Actions (TLA+)

An Anecdote Against Slop Artifacts

Domain-specific hyperspecialization (for SAT)

How to Find Bugs in Systems That Don't Exist

Why Rocq is better than Lean for program verification

A write-up on why I don't give in to the hype and switch to Lean for formal verification of programs. Comments

Fast DEFLATE compression in Lean

Xavier Leroy on programming, languages and formal verification

Extending MVCC to be serializable, in TLA+ (2024)

Introduction to Formal Verification with Lean (Part 1)

A Rust-to-Lean verification pipeline with AI provers: An experience report

Proving the Fundamental Theorem of Arithmetic in Agda

Formal methods and the future of programming

EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation

hax: A Rust verification tool

Announcing Isabelle support for SAW