Mastodawn

> A programming language designed for LLMs to write, not humans.

> The compiler verifies the contract via SMT solver.

Vera — A language designed for machines to write

A programming language where verification is a first-class citizen. Mandatory contracts, algebraic effects, typed slot references. Compiles to WebAssembly — runs at the CLI or in any browser.

Roger Sen 1d ago

To the #formalmethods community.

I have extensive programming experience and I want to get into #formalmethods, with the objective of formalising algorithms that work with time intervals.

I have started with Lean, but I have the feeling it is too low level for what I need.

What do you recommend?

Please re-tweet.

Lobsters 1d ago

How NASA Built Artemis II’s Fault-Tolerant Computer https://lobste.rs/s/nomyva #distributed #formalmethods #hardware #testing
https://cacm.acm.org/news/how-nasa-built-artemis-iis-fault-tolerant-computer/

How NASA Built Artemis II’s Fault-Tolerant Computer

0 comments

Lobsters

Lobsters 1d ago

Giving LLMs a Formal Reasoning Engine for Code Analysis https://lobste.rs/s/fu9wcm #formalmethods #vibecoding
https://yogthos.net/posts/2026-04-08-neurosymbolic-mcp.html

Giving LLMs a Formal Reasoning Engine for Code Analysis

2 comments

Lobsters

RSNikhil 4d ago

Heads-up: Mon Apr 13 (one week away): "FP Launchpad" kickoff-event at IIT Madras

FP Launchpad is a new research center at IITM focusing on all aspects of functional programming.

Schedule of talks, abstracts: https://fplaunchpad.org/2026/03/30/fp-launchpad-kickoff.html

#OCaml #OxCaml #Haskell #FormalMethods #HardCaml #Bluespec

FP Launchpad Kickoff

Centre for Functional Systems Research and Education at IIT Madras

FP Launchpad

Lobsters 6d ago

Functional Algorithms, Verified https://lobste.rs/s/lqthae #pdf #formalmethods #plt
https://www21.in.tum.de/teaching/fds/SS21/assets/book-draft.pdf

Functional Algorithms, Verified

0 comments

Lobsters

Lobsters Apr 3

Formal Methods https://lobste.rs/s/letcxt #formalmethods #plt
https://www.formalmethods.dk

Formal Methods

0 comments

Lobsters

Lean Apr 2

Lean 4.29.0 released with 453 changes.

Highlights: reduced startup time through static initialization of closed terms, simpler 𝚗𝚘𝚗𝚌𝚘𝚖𝚙𝚞𝚝𝚊𝚋𝚕𝚎 semantics improving predictability, higher-order Miller pattern support in 𝚐𝚛𝚒𝚗𝚍's e-matching engine, and a significant overhaul to instance and reducibility handling.

Full release notes: https://lean-lang.org/doc/reference/latest/releases/v4.29.0/

#LeanLang #LeanProver #FormalMethods

Lobsters Apr 2

Validating Hare’s Sort Module using Symbolic Execution via @RunxiYu https://lobste.rs/s/yoq0e6 #formalmethods #plt
https://notes.8pit.net/notes/y7n8.html

Validating Hare’s Sort Module using Symbolic Execution

0 comments

Lobsters

Christina Richards Apr 1

I know just enough mathematics to be dangerous – I formalized models of type systems as a grad student – but I like cute chalk mascots and thoughtful server rules, so hello!

Personal interests: choral singing, photography, poetry and vaguely gothic fiction, tinkering with formalisms

Professional interests: building reliable distributed systems; making legacy-horror DSLs spec-ful and debuggable

Nutrition facts: posts
Contains: #queer and #trans pride
May contain: lolwut

Follow requests are welcome, especially if we’ve interacted before.

#introduction #GothicFiction #DistributedSystems #ProgrammingLanguages #FormalMethods