Are you develping or using #FormalMethods?

Then #FM2026 is probably interested in your work!

Dates (AoE)
* Abstracts: 25th Nov 2025
* Papers 2nd Dec 2025
* Conference 20th–22nd May 2026
and Gold Open Access proceedings

Details:https://conf.researchr.org/track/fm-2026/fm-2026-research-paper

Are you develping or using #FormalMethods?

Then #FM2026 is probably interested in your work!

Dates (AoE)
* Abstracts: 25th Nov 2025
* Papers 2nd Dec 2025
* Conference 20th–22nd May 2026
Gold Open Access proceedings

Details:https://conf.researchr.org/track/fm-2026/fm-2026-research-paper

*Last Call*

I have a #PhD position for UK students, available with myself and @bentnib

This project will be looking at developing new methods for asserting the resilience of existing communicating systems by developing new static analysis methods derived from advanced programming language research.

*Hard Deadline*: Wednesday 16th April 2025

You will belong to @StrathCyber and @mspstrath, as well as gaining access to @spli

https://www.strath.ac.uk/studywithus/postgraduateresearchphdopportunities/science/computerinformationsciences/towardstype-drivenassuranceofcommunicatingsystems/

(Ignore the deadline on the advert)

Please spread the words.

"Verified" "Compilation" of "Python" with Knuckledragger, GCC, and Ghidra

https://www.philipzucker.com/knuckle_C_pcode/

Discussions: https://discu.eu/q/https://www.philipzucker.com/knuckle_C_pcode/

#formalMethods #gamedev #programming #commonLisp #acl2 #itch https://lispy-gopher-show.itch.io/lispmoo2/devlog/907091/formal-game-logic

Since yesterday I advocated strong use of defgeneric, defmethod and McCLIM's define-command, here I present

just giving lisp's defun to acl2's first order #logic.

I present a batch processing style for using acl2 both in #shell and in #lisp with a worked example.

Thoughts and opinions, gamedevs and logical types?

coq-of-rust: Formal verification tool for Rust

https://github.com/formal-land/coq-of-rust

Discussions: https://discu.eu/q/https://github.com/formal-land/coq-of-rust

Reading the new experience report paper "System Correctness Practices at AWS" by @marcbrooker & Ankush Desai, a successor to 2015 paper "How Amazon Web Services Uses Formal Methods". Documents a whole buffet of industrial formal methods use: P (including new tool PObserve for runtime trace validation), deterministic simulation testing in Rust with the open-sourced Shuttle and Turmoil tools, Dafny, HOL Light, and the open-sourced Kani model-checker for Rust.

While TLA⁺ was the most prominent featured tool in the 2015 paper, it's been lost in the crowd here as part of a clear shift toward verifying & testing the actual running code. I think TLA⁺ must carve out a niche for itself in a world where deterministic simulation testing becomes a commodity technology, or it risks losing relevance same as other design-level tools like UML. There are existing case studies on using TLA⁺ for trace validation and model-driven testing, but a lot of effort needs to go into tooling for making such integrations as smooth as possible instead of bespoke one-off projects.

https://dl.acm.org/doi/10.1145/3712057

From August 11-14 we're going to be holding a UC (Universally Composable Security)/EasyUC Summer School at Boston University.

Here is a preliminary announcement:

https://alleystoughton.us/UC-EasyUC-summer-school-save-the-date-flyer.pdf

If you might be interested in participating in the summer school, we hope you will put yourself on our mailing list and give us feedback that will help us fine tune our plans for the school.

You can also email the organizers at

uc-easyuc-summer-school+owners@googlegroups.com

Systems Correctness Practices at AWS: Leveraging Formal and Semi-formal Methods https://lobste.rs/s/pyjpo3 #formalmethods
https://dl.acm.org/doi/pdf/10.1145/3712057

I have a funded #PhD position for UK students, available with myself and @bentnib

This project will be looking at developing new methods for asserting the resilience of existing communicating systems by developing new static analysis methods derived from advanced programming language research.

Deadline: Thursday 20th March 2025

You will belong to @StrathCyber and @mspstrath, as well as gaining access to @spli

For now more details about the project are on my personal website.

https://tyde.systems/page/position/2025-jarss/

Please spread the words.

We are Formal Methods Europe, an association promoting research and practice in #FormalMethods mathematical #SoftwareEngineering approaches that support the rigorous specification, design and verification of systems.

Find out more here: https://www.fmeurope.org/

Verify the Safety of the Rust Standard Library

https://aws.amazon.com/blogs/opensource/verify-the-safety-of-the-rust-standard-library/

Hey You'se!

Applications for PhD scholarships (UK students fully funded, international students part funded) in Computer & Information Sciences at Strathclyde are *open*.

Details on applications within @mspstrath are here:

https://msp.cis.strath.ac.uk/phd2025-JARSS.html

*Deadline* 25th November, 2024.

Please share!

"With mathematics, we can predict the behavior of systems before a single line of code is written." - Marc Brooker, VP/Distinguished Engineer at AWS

Excited to have @shriramk in CU Boulder's CS Dept Colloquium (in-person & online) April 23, 2024! Presenting on the Human Factors of Formal Methods.

https://calendar.colorado.edu/event/cs-colloquium-shriram-krishnamurthi-on-the-human-factors-of-formal-methods

Creusot, a deductive verifier for Rust code

https://github.com/creusot-rs/creusot

Discussions: https://discu.eu/q/https://github.com/creusot-rs/creusot