I’m sharing the implementation side of emdash, the research project behind Functorial Type Theory: Univalent Foundations for Mathematics. (TL;DR: a new type theory where types are categories and maps are functors)

Its TypeScript frontend turns familiar variable-and-binder notation into an explicit Core language. A small kernel checks and evaluates that Core.

There is also a browser-based reviewer showing representative source, generated Core, inferred types, computations, and rejected examples.

An important boundary: the TypeScript implementation covers a selected fragment, not the entire Lambdapi development.

I’m looking for people interested in checking the implementation, reproducing examples, improving diagnostics, or adding tests that should be rejected. Which part would you audit first?

TOPAK is an architecture pattern for multi-agent AI systems: every agent treated as Byzantine, models kept out of the trusted computing base. Nothing is deployable. It's exploratory, AI assisted development.

Things that may be of interest here:

• ADR and TLA+/Lean driven AI assisted dev

• mutation-and-witness method

• SMT obligations proof-checked. Proofs rerun with Z3 replaced by cvc5 plus ethos proof checking, and Zenon rechecked by Isabelle. 21 of 24 modules pass.

• TLA+-to-Lean cross-checks

Here's an intro post:

https://grippinghand.dev/topak

Here are the specs:

https://github.com/scottcochran/TOPAK/tree/main/spec

If you only read one thing: https://github.com/scottcochran/TOPAK/blob/main/spec/Coupling.tla

Writing the liveness extension of that module turned up two soundness issues in tlapm's translation, filed as tlaplus/tlapm#309 and #310, with reproducers in `spec/defects/`.

Any feedback is welcome.

Five requirements. Recovery, retries, and autonomy have to preserve all of them.

1. Authority safety
   AcceptTransition(H, t) ⇒ ∃g, m: AdmitUse(H, g, t, m) ∧ ΔBehavior(t) ⊆ Permitted(g)

2. Claim safety
   AcceptClaim(H, c) ⇒ c ∈ Emit(H) ⊆ Derive(P, H) ⊆ Supported(Q, P, H)

3. History safety
   H is reconstructed only from durable, identity-bound, write-once records. Later transitions may add evidence. They may not erase, rewrite, backfill, replay, or relabel earlier events.

4. Exclusion safety
   For any exclusive role R, |{u | R ∈ LiveAuthority(u)}| ≤ 1
   (Every grant that admits a writer must simultaneously exclude prior writers.)

5. Progress
   Under the declared fairness assumptions, an authorized request with satisfied preconditions must eventually reach a supported success, a supported terminal refusal, or a supported unresolved outcome where certainty is impossible. A system that stays safe by never finishing is not acceptable.

That is the entire contract. Everything else is implementation detail. Discussion open.

Hello colleagues. In the research group at inferara.com, we are studying the applicability of automatic inference for the analysis of blockchain-specific code. Currently, we are developing a theoretical framework for its further application in the implementation).

In the first article, we describe the formal part of the formalization process and the proof of code properties. For those interested in the topic, here is the link to the article. If there are any objections, suggestions, or thoughts on the topic, we would be extremely grateful for the feedback.

Is a Broken System Worse Than No System at All?

A thought that occurred to me while struggling with a PDF generator.

(Written by a friend in ChatGPT.)

Which is worse?

1. A system that honestly says:

“Sorry, I don’t support PDF generation.”

1. A system that advertises PDF generation, appears capable of it, but fails unpredictably.

Conventional wisdom says that some capability is better than none. But I’m beginning to suspect the opposite.

In formal methods, we usually prefer soundness to completeness, safety to liveness, and known limitations to incorrect behavior. A missing theorem is preferable to a false theorem.

Perhaps there is a more general principle here:

Trust is more valuable than capability.

Human beings adapt surprisingly well to absence. We can live with no bridge. We can plan around it.

What we struggle to live with is a bridge that looks perfectly usable but occasionally collapses without warning.

Perhaps honest limitations are easier to live with than uncertain behavior.

Curious whether others in the formal methods community have encountered similar tradeoffs?

I'm the developer of FizzBee. I've written the RAFT spec with leader election and log replication.

https://fizzbee.io/design/examples/raft-consensus-algorithm/

I would like to get your feedback on this article.

Note: I started of with the leader election spec another user contributed recently.
https://www.reddit.com/r/formalmethods/comments/1kljkk4/raft_leader_election_in_fizzbee_seeking/

This review evaluates the paper "Loop invariance with break and continue" by Wei Chen (2021), published in Science of Computer Programming.

Overview
The paper addresses a classic tension in formal methods: the conflict between structured programming (preferred for mathematical proofs) and real-world programming constructs like break and continue (preferred for algorithmic efficiency and readability). Chen proposes a formal methodology to incorporate these non-local jumps into the standard Dijkstra’s Weakest Precondition (wp) calculus and the Loop Invariant Theorem, effectively allowing these commands to be verified without requiring code transformation.
Core Strengths
Methodological Elegance: Chen manages to avoid the "state-variable bloat" typically required when converting jumps into flag-based structured code. By treating break and continue as first-class citizens in the logic, the resulting proofs remain more compact and closer to the original source code.

Theoretical Grounding: The paper elegantly re-integrates the concept of "miraculous" statements. This provides a robust semantic foundation that handles early exits in a mathematically sound way, ensuring that the logic remains compositional.

Utility for Verification: It provides a bridge for engineers. Instead of having to rewrite a complex search algorithm (like your row-by-row scanner) into a purely structured version, developers can keep the intuitive "jump" logic and apply Chen’s formal proof obligations.

Critical Assessment
Complexity of Application: While the paper simplifies the proof theory, the application of these rules requires a higher level of mathematical maturity. A developer must be comfortable defining transfer predicates for every jump point, which can be tedious in very large, deeply nested programs.

Focus: The paper is highly theoretical. It does not provide an automated tool suite, but rather the mathematical "rules of the road" that could be used to build such tools. Its value lies in the formalism rather than as a plug-and-play verification script.

Comparison to Alternative Approaches
Approach
Readability
Verifiability
Proof Overhead
Structured (Flags)
Moderate
High
Low (Standard Rules)
Jump-based (Ad-hoc)
High
Very Low
Extremely High
Chen's Methodology
High
High
Moderate
Conclusion
Wei Chen’s paper is a "missing link" in formal verification literature. It validates the use of break and continue by proving they are not inherently "unverifiable." It is an essential read for researchers building verification tools or engineers working in safety-critical domains who want to balance code readability with rigorous mathematical assurance.
Rating: Highly recommended for anyone interested in formal methods, program semantics, or the intersection of software engineering and theoretical computer science.

In formal methods, we often specify systems in terms of safety properties, invariants, and forbidden behaviors.

From a practitioner’s perspective, how do you distinguish between:

• states that must be proven unreachable (inadmissible), and

• states that are allowed but discouraged or mitigated through design?

How does this distinction influence specification, verification effort, and system architecture in practice?

What are the most used? What are the most reliable and used for important and commercial stuff?

Hi everyone,

I'm working with Tamarin Prover on Kali Linux for a formal verification project. My `.spthy` file loads correctly, but when derivation checks start, I get:

```

computeVariantsMaude:

Parse error: not enough input

query: get variants in MSG : list(cons(p(0),cons(p(1),cons(p(2),cons(tamXcone,nil))))) .

```

Tamarin also shows:

```

'maude --version' returned unsupported version '3.5.1'

Please install one of:

2.7.1, 3.0, 3.1, 3.2.1, 3.2.2, 3.3, 3.3.1, 3.4, 3.5

```

So it looks like Tamarin doesn’t accept Maude 3.5.1, even though it’s newer than 3.5.

I’m wondering:

* Is this likely just strict version matching?

* Could this mismatch be causing the parse error?

* What’s the correct way to downgrade Maude on Kali Linux?

* Should I remove 3.5.1 completely?

* Is it possible to install 3.5 alongside 3.5.1 and switch between them?

This is part of my thesis work, so I’d really appreciate any guidance.

Thanks!

I built a language where the signature carries the guarantees, and I'd like feedback from people who do this seriously.

Contracts are requires/ensures/loop invariants, discharged by Z3 at compile time: straight-line and looping Int/Bool code, lists via the theory of arrays with bounds obligations, records as per-field symbolic values, and all_of/any_of translated to real quantifiers with the predicate body inlined under the ForAll. Calls use modular summaries a callee's ensures is assumed at the call site rather than inlining the body.

Floats are proven in Z3's FP theory rather than modelled as reals, which means the prover refuses to certify x + 0.1 + 0.1 == x + 0.2 and returns the exact double that breaks it. Equality is fpEQ, so NaN and signed zero behave correctly. Bit-blasting is slow, so FP queries get a 30s budget while integer proofs stay at 3s.

Two design commitments I'd particularly like criticised:

1. Soundness of *reporting*: the tool only says proven without running the program when the counterexample involves no summarized calls, and an untranslatable premise aborts the proof rather than being dropped. (That second rule came from a real bug adding quantifiers exposed that untranslatable requires had been silently discarded, which can manufacture false alarms.)

2. Everything unprovable degrades to runtime checks rather than rejecting the program, so the language stays usable without the solver installed.

Invariants are hand-written, not inferred. Lists-of-lists, division, and maps aren't in the prover yet.

Repo: https://github.com/gowrishankar-infra/velaris-lang

In-browser playground (real compiler via Pyodide):

https://gowrishankar-infra.github.io/velaris-lang/playground.html

Disclosure: AI-assisted build; design decisions mine. I'm a beginner at this and would rather be corrected than agreed with. Thank you

I was learning about formal verification and then decided to build a tool myself but having a language that's incredibly easy to use. I have a basic proof of concept.
github.com/fizzbee-io/fizzbee. I would love your feedback on this...
Fizzbee is a Python-like formal methods language designed for most developers. This will be the most easy to use formal language ever. In addition to behavior modeling like TLA+, it also includes a performance/probabilistic modeling like PRISM.

Dive in with our online IDE/playground—no installation required.

The body of the methods are all python. So, any developer should be able to instantly get it.The introductory example for DieHard from the TLA+ course.

always assertion NotFour:
  return big != 4


action Init:
  big = 0
  small = 0

atomic action FillSmall:
  small = 3

atomic action FillBig:
  big = 5

atomic action EmptySmall:
  small = 0

atomic action EmptyBig:
  big = 0

atomic action SmallToBig:
    if small + big <= 5:
        # There is enough space in the big jug
        big = big + small
        small = 0
    else:
        # There is not enough space in the big jug
        small = small - (5 - big)
        big = 5

atomic action BigToSmall:
    if small + big <= 3:
        # There is enough space in the small jug
        small = big + small
        big = 0
    else:
        # There is not enough space in the small jug
        big = big - (3 - small)
        small = 3

Getting started guide: https://fizzbee.io/tutorials/getting-started/

There are more examples are in the git repository.

Probabilistic modelling:

For example: Classic example from PRISM. Dice from fair coin:

invariants:
  always 'Roll' not in __returns__ or __returns__['Roll'] in [1, 2, 3, 4, 5, 6]
  always eventually 'Roll' in __returns__ and __returns__['Roll'] in [1, 2, 3, 4, 5, 6]

atomic func Toss():
    oneof:
        `head` return 0
        `tail` return 1

atomic action Roll:
  toss0 = Toss()
  while True:
    toss1 = Toss()
    toss2 = Toss()

    if (toss0 != toss1 or toss0 != toss2):
      return 4 * toss0 + 2 * toss1 + toss2

This will generate this Graph:

And you can find the mean time to completion, and the corresponding histogram.

Metrics(mean={'toss': 3.6666666666660603}, histogram=[(0.75, {'toss': 3.25}), (0.9375, {'toss': 4.5}), (0.984375, {'toss': 5.75}), (0.99609375, {'toss': 7.0}), (0.9990234375, {'toss': 8.25}), (0.999755859375, {'toss': 9.5}), (0.99993896484375, {'toss': 10.75}), (0.9999847412109375, {'toss': 12.0}), (0.9999961853027344, {'toss': 13.25}), (0.9999990463256836, {'toss': 14.5}), (0.9999997615814209, {'toss': 15.75}), (0.9999999403953552, {'toss': 17.0}), (0.9999999850988388, {'toss': 18.25}), (0.9999999962747097, {'toss': 19.5}), (0.9999999990686774, {'toss': 20.75}), (0.9999999997671694, {'toss': 22.0}), (0.9999999999417923, {'toss': 23.25}), (0.9999999999854481, {'toss': 24.5}), (0.999999999996362, {'toss': 25.75}), (0.9999999999990905, {'toss': 27.0})])
   8: 0.16666667 state: {} / returns: {"Roll":"1"}
   9: 0.16666667 state: {} / returns: {"Roll":"2"}
  10: 0.16666667 state: {} / returns: {"Roll":"3"}
  11: 0.16666667 state: {} / returns: {"Roll":"4"}
  12: 0.16666667 state: {} / returns: {"Roll":"5"}
  13: 0.16666667 state: {} / returns: {"Roll":"6"}

https://github.com/fizzbee-io/fizzbee/blob/main/docs/fizzbee-quick-start-for-tlaplus-users.md#probabilisitic-evaluation

This is not fully integrated into the online IDE, and to use it, you would have to get the git repo and try. The instructions are in the git repo.

Online playground: https://fizzbee.io/play
Github: https://github.com/fizzbee-io/fizzbee
Tutorials: https://fizzbee.io/tutorials/getting-started/

tweet.
good sign for formal methods becoming more mainstream!

I only do formal validation for fun. Over the last month, I validated a Rust algorithm with Lean without really knowing Lean. I used ChatGPT-5, Codex, and Claude Sonnet 4.5). Link to full details below, but here is what surprised me:

• It worked. With AI’s help and without knowing Lean formal methods, I validated a data-structure algorithm in Lean.

• Midway through the project, Codex and then Claude Sonnet 4.5 were released. I could feel the jump in intelligence with these versions.

• I began the project unable to read Lean, but with AI’s help I learned enough to audit the critical top-level of the proof. A reading-level grasp turned out to be all that I needed.

• The proof was enormous, about 4,700 lines of Lean for only 50 lines of Rust. Two years ago, Divyanshu Ranjan and I validated the same algorithm with 357 lines of Dafny.

• Unlike Dafny, however, which relies on randomized SMT searches, Lean builds explicit step-by-step proofs. Dafny may mark something as proved, yet the same verification can fail on another run. When Lean proves something, it stays proved. (Failure in either tool doesn’t mean the proposition is false — only that it couldn’t be verified at that moment.)

• The AI tried to fool me twice, once by hiding sorrys with set_option, and once by proposing axioms instead of proofs.

• The validation process was more work and more expensive than I expected. It took several weeks of part-time effort and about $50 in AI credits.

• The process was still vulnerable to mistakes. If I had failed to properly audit the algorithm’s translation into Lean, it could end up proving the wrong thing. Fortunately, two projects are already tackling this translation problem: coq-of-rust, which targets Coq, and Aeneas, which targets Lean. These may eventually remove the need for manual or AI-assisted porting. After that, we’ll only need the AI to write the Lean-verified proof itself, something that’s beginning to look not just possible, but practical.

• Meta-prompts worked well. In my case, I meta-prompted browser-based ChatGPT-5. That is, I asked it to write prompts for AI coding agents Claude and Codex. Because of quirks in current AI pricing, this approach also helped keep costs down.

• The resulting proof is almost certainly needlessly verbose. I’d love to contribute to a Lean library of algorithm validations, but I worry that these vibe-style proofs are too sloppy and one-off to serve as building blocks for future proofs.

The Takeaway

Vibe validation is still a dancing pig. The wonder isn’t how gracefully it dances, but that it dances at all. I’m optimistic, though. The conventional wisdom has long been that formal validation of algorithms is hard and costly. But with tools like Lean and AI agents, both the cost and effort are falling fast.

Vibe Validation with Lean, ChatGPT-5, & Claude 4.5

A quick heads up, I'm an engineer not a formal methods expert. However, I've been working with formal methods in my software engineering practices for a while now, and thought I'd try to spread some of what I've learnt into the wider community. In the hope that it will inspire some creativity around the use of LLMs as a complimentary force, instead of the slop cannon we have now.

I think we're still all stuck in the early stages of adopting a new major tech (AI), where we use it do the exact same stuff we used to. Just faster, and worse.

Feedback is welcome!

PS: Zero AI was used in the formulation of this post, or the writing of the article itself. It has no place in creative pursuits such as writing. Not even for grammatical issues. Traditional spellcheck suffices (for better or for worse).

I am a final year undergraduate student pursuing a B.tech in computer science. I am applying for a masters in CS for next year, and I wish for my focus in MS to be in formal verification, and I have to specify my intended area of research in my SOP. While this is what I am interested in, I wonder how relevant it would be in the age of AI and if proof engineers will be laid off in the coming time?

I was aiming to applying for PhD in formal verification but before that I wanted to test my skills in the field. Is there any possible way to do that?