Recent searches

No recent searches

Search options

Not available on photog.social.
photog.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
A place for your photos and banter. Photog first is our motto Please refer to the site rules before posting.

Administered by:

Server stats:

244
active users

photog.social: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.3

#formalverification

0 posts0 participants0 posts today
*
Jan :rust: :ferris:

ESBMC - An Efficient SMT-based Bounded Model Checker

ssvlab.github.io/esbmc/

"ESBMC is an open-source, [...], context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs. It does not require the user to annotate the programs with pre- or postconditions, but allows the user to state additional properties using assert-statements, that are then checked as well."

1/3

ESBMCESBMC: An Industrial-Strength C Model CheckerSMT-based Context-Bounded Model Checker for C Programs.
#SMT#FormalVerification#FormalMethods
*
Jan :rust: :ferris:

Verifying the #Rust Standard Library - Carolyn Zech, Amazon Web Services

invidious.nerdvpn.de/watch?v=8
(or YT: youtube.com/watch?v=8_lzVNs1uPk)

Carolyn is also a maintainer of #Kani, the Rust model checker.
She has been so supportive and kind during my struggles with HashMaps and Kani 🥺

github.com/model-checking/kani

Give her a follow:
github.com/carolynzech

invidious.nerdvpn.deabominable, devilish rebellion against the gunwale, tumbled back to the immaculate
#FormalVerification#FormalMethods#RustLang
Jan :rust: :ferris:

@d10c4n3

Yes, this is another issue with the current #LLM architecture: they can't learn or improve. It's one big monolith - not composed of smaller parts (that could individually be improved or composed with each other).

There _are_ AI architectures that are _actually reliable_...

floss.social/@janriemer/114454

...but our industry has decided to hyperfocus on bullshit machines.

@larsmb

FLOSS.socialJan :rust: :ferris: (@janriemer@floss.social)@jasongorman@mastodon.cloud @hakona@im.alstadheim.no @omegaprobe@neopaquita.es It's such a shame that focus is so much on LLMs these days. There are _very_ promising, alternative approaches that are _actually reliable_. One is called model-based reasoning. I've first written about it at the end of 2022: https://floss.social/@janriemer/109480193245545801 Recently, I've found out about Automatic Reasoning. I had some interesting conversations about it here: https://floss.social/@janriemer/114224822632574083 I can highly recommend both threads. 🤓
#ArtificialIntelligence#FormalVerification
Jan :rust: :ferris:

Owi

github.com/OCamlPro/owi

Symbolic execution for #Wasm, #C, C++, #Rust and #Zig

"#Owi is an open-source framework for advanced #WebAssembly analysis and manipulation, with a focus on practical symbolic execution and robust tooling. It is designed for researchers, engineers, programming language enthusiasts and practitioners requiring precise, flexible, and extensible support program reasoning."

GitHubGitHub - OCamlPro/owi: Symbolic execution for Wasm, C, C++, Rust and ZigSymbolic execution for Wasm, C, C++, Rust and Zig. Contribute to OCamlPro/owi development by creating an account on GitHub.
#FormalVerification#SoftwareTesting#Testing
Replied in thread
Jan :rust: :ferris:

@sabik @dequbed @eniko @pixel

Totally agree! Unit tests and usage of #LLMs in that area are a bad combo (both for implementation and tests).

However, I'd like to give you some "food for thought":
What if the LLM was generating code against a (human written) #proof?

See this blog post, where they've written a proof with #Kani, a model checker in #Rust and let the #LLM generate the implementation until the proof passes:

model-checking.github.io/kani-

Kani Rust Verifier Blog · Writing Code with ChatGPT? Improve it with Kani.Kani is a verification tool that can help you prove properties about your Rust code. To learn more about Kani, check out the Kani tutorial and our previous blog posts.
#FormalVerification#RustLang
Jan :rust: :ferris:

People of ACM - Derek Dreyer

acm.org/articles/people-of-acm

"Derek Dreyer is a Scientific Director at the Max Planck Institute for Software Systems (MPI-SWS) [...]. His [...] interests include type systems, semantics of programming languages, verification of concurrent programs, and interactive theorem proving. [...] His goal is “to produce rigorous formal foundations for establishing the safety and reliability of software systems.”"

www.acm.orgPeople of ACM - Derek DreyerDerek Dreyer is a Scientific Director at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbrücken, Germany. At MPI-SWS, he leads the Foundations of Programming Group. His broad range of interests include type systems, semantics of programming languages, verification of concurrent programs, and interactive theorem proving. In his research statement, Dreyer writes that his goal is “to produce rigorous formal foundations for establishing the safety and reliability of software systems.”
#FormalVerification#Rust#RustLang
Jan :rust: :ferris:

(❁´◡`❁)

#Rust pattern types RFC:
gist.github.com/joboet/0cecbce

Pattern types are a form of refinement types, which allow some subset of #FormalVerification!

en.wikipedia.org/wiki/Refineme

Tracking Issue for #PatternTypes:
github.com/rust-lang/rust/issu

Tracking Issue for generic pattern types OwO:
github.com/rust-lang/rust/issu

Implement minimal, internal-only pattern types in the type system:
github.com/rust-lang/rust/pull

I'm _really_ looking forward to how #RustLang will evolve in this area!👀

GistPattern types RFCPattern types RFC. GitHub Gist: instantly share code, notes, and snippets.
#ProgrammingLanguage
Lean

The Department of Computer Science, University of Oxford has released recordings of the recent Strachey Series Lectures featuring Leo de Moura and Kevin Buzzard:

1️⃣ "Formalizing the Future: Lean's Impact on Mathematics, Programming, and AI" - Leo de Moura, Chief Architect of Lean

Leo discusses how Lean provides a framework for machine-checkable mathematical proofs and code verification, enabling collaboration between mathematicians, software developers, and AI systems. He also outlines the work the Lean Focused Research Organization does to expand Lean’s capabilities and support the community.

➡️ Watch Leo's lecture here: podcasts.ox.ac.uk/formalizing-

2️⃣ "Will Computers Prove Theorems?" with Kevin Buzzard, Professor of Mathematics, Imperial College

Kevin examines the potential for AI systems and theorem provers to assist in mathematical discovery, addressing whether computers might someday find patterns in mathematics that humans have missed, and discusses the integration of language models with formal verification systems.

➡️ Watch Kevin's lecture here: podcasts.ox.ac.uk/will-compute

podcasts.ox.ac.ukFormalizing the Future: Lean’s Impact on Mathematics, Programming, and AIHow can mathematicians, software developers, and AI systems work together with complete confidence in each other’s contributions? The open-source Lean proof assistant and programming language provides an answer, offering a rigorous framework where proofs and programs are machine-checkable, shared, and extended by a broad community of collaborators. By removing the traditional reliance on trust-based verification and manual oversight, Lean not only accelerates research and development but also redefines how we collaborate.
#LeanLang#LeanProver#FormalVerification
Jan :rust: :ferris:

F* (fstar) Interactive Tutorial:

fstar-lang.org/tutorial/

I'm only like 10% into the tutorial, but this language is CRAZY (fun)! :awesome: 😄

I try to learn the fundamentals of it, so I can use the backend of it in #Aeneas... so I can ultimately formally verify my #Rust crate (former attempts with #Creusot and #Kani failed for me).

Aeneas:
github.com/AeneasVerif/aeneas

See part two of toot for a toy example of proving function equivalence

1/2

fstar-lang.orgF* Tutorial
#FormalVerification#FunctionalProgramming#RustLang
Continued thread
Jan :rust: :ferris:

Huh, seems like I really have been living on the bleeding edge (of #FormalVerification):

github.com/creusot-rs/creusot/

The verification in the prev toot is currently not possible in #Creusot due to missing specs for the `Hash` trait and HashMap more broadly. 😔

Oh well, seems like (at least currently!) I won't be able to fully verify the diffing algorithm of #CSVDiff.🥺

Options I have now are:
- Only verify parts of the algorithm (that don't depend on HashMap ops)
or
- Use fuzzing/property testing

GitHubTimeout when trying to verify `add` operation on HashMap newtype · creusot-rs creusot · Discussion #1477Hi all, disclaimer: I'm totally new to formal verification and creusot, so bear with me 😄 I try to verify a simple add operation on a HashMap newtype (see code below), but it seems I run into a tim...
Jan :rust: :ferris:

Place Capability Graphs: A General-Purpose Model of #Rust’s
Ownership and Borrowing Guarantees (April 2025)

arxiv.org/pdf/2503.21691

"We present a novel model of Rust’s type-checking [...], which lifts [...] limitations [of current verification tools], and which can be directly calculated from the #RustLang compiler’s own programmatic representations and analyses. We demonstrate that our model supports over 98% of Rust functions in the most popular public crates...

1/2

#FormalVerification
Continued thread
Jan :rust: :ferris:

Re: Help us create a vision for Rust's future 👆

In the mid- to long-term I can see #Rust focus more and more on facilitating #FormalVerification - it perfectly aligns with #RustLang's vision of enabling everyone to build _reliable_ and efficient software.

First step is probably to have a common contract language, which might enable interoperability of different verification tools.

(Disclaimer: I'm a total newbie in the field of formal verification, but I find it absolutely fascinating!)

Live feeds
About