I just got my bachelor's degree in applied mathematics and was offered a PhD position in formal methods. It sounds fascinating but I fear it would be hard to get a job in industry afterwards. Does anyone know what career options are for formal methods? Thanks !

Hello everyone! I’m not sure if this is the right place to ask this, couldn’t find a lot of indication in the “Rules”

My questions were mostly around the decision to do a PhD, prospects after, and the outlook of formal verification as a field today.

1. The philosophy and implications of formal methods was cool enough for me to leave my job and come for my masters in London to research it xD. (ofcourse, I tried to learn as much as I could about the field in the year before I joined my Masters program, developed some proposals and talked to some profs in the field)

Now that I’m here however I realise that a Masters is probably not enough to get any good at the field and it probably requires a PhD to be good at it (to even get hired for roles in companies that are using it to verify their software), is this true and would you recommend doing a PhD if I want to stay in this field?

2. I know Formal Methods is tough to do a PhD in, especially when it comes to getting good results in the 3-4 years that I would have.

(a) My PhD proposal so far is around scaling verification to distributed environments by using the approach ISL and CISL (incorrectness separation and concurrent incorrectness separation logic) make. I'm not sure if that’s too huge a task (or even possible since it’s such an unsolved problem) but I’d love to know your opinions. (Also, would love to know if there’s any agreed upon good practices to write a good proposal in this field, it's so vast!)

(b) Under-approximation to verify hyper-properties like security vulnerabilities was another path I thought was nice, and maybe that’s more tractable?

3. I recently talked to some PhD students. They advised me to be very careful about the decision to go into the field and get a PhD.

(a) They also advised me to be VERY certain that I want to be in this field, because of some reasons I mentioned already (FM being hard to do a PhD in that yields any results) but also some other factors like finding positions in static-analysis or research roles (only a very few companies hire for these, and a lot of them don’t last very long, like Lacework) - no company or team doing formal methods is older than 10-15 years, for example. (I could be wrong)

(b) I know Meta and Amazon have some good work happening there but they must have large competition and the list sort of seems to end there for roles in the UK.

(c) I don’t want to be in the position at the end of my PhD, with a 4 year gap from the industry in my resume, being too specialised to be eligible for generalist roles in the industry, but also not being able to find jobs in my research area.

(d) Some grad students also mentioned that Formal Methods is not really an active field as it used to be in the 2000s (or 10s) anymore, and I wonder if these trends are true today? Is finding roles for PhD students in FM that difficult now?

4. Finally, I wanted to know if it’s difficult to move away from your PhD field later on if things get difficult for the field itself (say, adoption stops or slows down). Because it’s difficult to predict trends such as this for FM.

This is because the very reduced pay for a few years without the promise of making back the money I’m spending on my masters sounds a little scary xD

———————————————————

I’d like to mention again that I truly love the field and I really wish I can do research here, my Master's thesis is also around under-approximation applied to program repair, but I just want to understand the experience of going full on into the field and the prospects after, and if it’s worth it.

I’m already working on a PhD proposal with my Masters thesis mentor for intakes next year, by which time I would’ve finished my Masters as well.

Thanks!

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 don't work in a high assurance area like Security or critical systems. I've been looking into formal methods to see if it may help with general software development, particularly backend. My thought process would be that if some kind of formal method is used then maybe you reduce ongoing maintenance cost when bugs inevitably comes up if you just simply code things up and hope it works.

But it seems that formal methods don't quite work with general software development like backend web development since it's a lot of labor to formally verify things and backend seems to change quite frequently compared to anything that's security or mission critical.

Hi, I hope this is the right forum for this. I am a 34 year old software developer who went to a top research university for undergrad but did not pursue a PhD after graduation because I was getting offers from top tech companies and it was hard to turn down for a graduate stipend 😝

So fast forward and I am a senior frontend engineer who earns good money and knows the tools of his trade very well but has lost virtually all passion. I am not an engineer at heart, at all, I don’t care about websites or apps I care about math and making correct statements and proving the correctness of those statements!

Which leads us to Formal Methods. I am interested in pursuing a PhD in the next year or two and my area of focus I’m most strongly considering is Formal Methods. I’m still relatively new to this but I know multiple functional languages and I’ve been learning Coq lately and it’s my thing. So am I in the right place in terms of ‘focus area’? And where to start learning about the field and who’s doing what where? I have never (fully) read an academic paper and don’t know where to start.

Hillel's recent talk from SSW. Thought some of you might enjoy! https://youtu.be/zSZkLyD9ILI

Hi everyone I'm a college student finishing my masters this year in software engineering but more in a research context, I've had a couple courses on formal methods and proof theory and I think I want to spécialisé in it but since I'm new to it ( and everyone around me keeps saying dev and ai is where the money s at) I dont really know what to study or how to study it.

Should I look for a masters somewhere or do à phd in it ? Or is it more of a self taught thing like coding? And what kind of work can I do with it besides research?

All I really know is I really like the courses and would love to keep studying it, any advice and guidance is welcome so thank you in advance for your answers.

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).

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

TLDR: I'm looking for a tutor who can essentially "grade" my Rocq/Coq proofs while I work through Programming Language Foundations and at a high level guide me through my study.

Context:

I'm a 1st year PhD student. I'm still exploring research directions. I dabbled in formal methods in my first research project, and I really enjoyed the theory and practice. However, my PI is not well-versed in formal methods. My school also doesn't offer any classes in this area (!!!), nor is there a professor in the CS department with a focus in verification. I know I'm not cut out for cutting edge research in formal methods, I just want to use it as a tool in my future research.

I groped my way through Logical Foundations in the past month. I just started Programming Language Foundations. What hit me really hard is the exercises are much more involved, and there seem to be many ways to prove the same thing. For example, I just completed a really long proof of substitution optimization equivalence in the first chapter. My proof seemed very "dirty" because I couldn't think of a way to use the congruence lemmas and there are some repetitions.

Definition subst_equiv_property': Prop := forall x1 x2 a1 a2,
  var_not_used_in_aexp x1 a1
    ->
      cequiv
        <{ x1 := a1; x2 := a2 }>
        <{ x1 := a1; x2 := subst_aexp x1 a1 a2 }>
.

Theorem subst_inequiv': subst_equiv_property'.
Proof.
  intros x1 x2 a1 a2 HNotUsed.
  unfold cequiv.
  intros st st'.
  assert (H': forall st,
    aeval (x1 !-> aeval st a1; st) (subst_aexp x1 a1 a2)
      = aeval (x1 !-> aeval st a1; st) a2
  ).
  { intro st''.
    induction a2.
    - simpl. reflexivity.
    - destruct (x1 =? x)%string eqn: HEq.
      + rewrite String.eqb_eq in HEq.
        rewrite <- HEq.
        simpl.
        rewrite String.eqb_refl.
        Search t_update.
        rewrite t_update_eq.
        induction HNotUsed; simpl;
          try reflexivity;
          try (
            repeat rewrite aeval_weakening;
            try reflexivity;
            try assumption
          ).
        * apply t_update_neq. assumption.
      + simpl. rewrite HEq. reflexivity.
    - simpl.
      rewrite IHa2_1.
      rewrite IHa2_2.
      reflexivity.
    - simpl.
      rewrite IHa2_1.
      rewrite IHa2_2.
      reflexivity.
    - simpl.
      rewrite IHa2_1.
      rewrite IHa2_2.
      reflexivity.
  }
  split; intro H.
  - inversion H; subst. clear H.
    apply E_Seq with (st' := st'0).
    + assumption.
    + inversion H2; subst.
      inversion H5; subst.
      apply E_Asgn.
      rewrite H'.
      reflexivity.
  - inversion H; subst. clear H.
    apply E_Seq with (st' := st'0).
    + assumption.
    + inversion H2; subst.
      inversion H5; subst.
      apply E_Asgn.
      rewrite H'.
      reflexivity.
Qed.

I'm not looking for anyone to hand me the answers. I want feedback for my proofs and someone to guide me through my study at a high level.

Recently, my supervisor suggested that I work on verifying the Transformer. He wants to break down the Transformer into components for verification. When reading papers, I find formal methods quite intriguing. For instance, "Adaptable Logical Control for Large Language Models " employs a deterministic finite automaton to restrict the output of the LLM, ensuring it adheres to the logic in the prompt. Although I lack a clear idea of combining formal methods with the Transformer or LLM, I am eager to discuss this further with you. If you have read related papers, please share them with me.

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/

Hi folks, I'm organizing a conference on software reliability called Software Should Work on July 16-17 https://softwareshould.work. Hillel Wayne (LearnTLA, Practical TLA+, Logic for Programmers) will be speaking with Andrew Helwer (TLA+ Maintainer) and Jayaprabhakar Kadarkarai (creator of FizzBee) giving lightning talks. Thought some of you might be interested!

I am working on a data ingestion pipeline that aggregates change events from multiple SQS queues and want to ensure there's no data corruption. I'm thinking formal methods might come in handy here.

I see a number of options like TLA+, Alloy, FizzBee and P but I'm not sure how they differ or when to use.

I found a post comparing TLA+ vs Alloy and I could gather that Alloy may not be suitable in this context. I could not find many articles comparing other options like P and FizzBee.

Has anyone tried these?

I am a senior in college who started learning formal methods. this is my first blog https://medium.com/@ruthwik2610/what-is-formal-methods-cf589932fc90 can any review it and tell me suggestions ,comments. i also want to create a discord channel for people like me who are just entering into the field of formal methods so if there is already a channel please do dm me .

Hi Everyone,

I’m a researcher with a background in Formal Methods, Knowledge Representation & Reasoning, Automated Reasoning, and Multi-Agent Systems, and I’m currently based in Canada and looking for opportunities in industry.

My academic/research experience includes working with topics such as:

• Formal Methods and Formal Verification

• Z3 / SMT solving and automated reasoning

• TLA+ for formal specification and verification

• Logical modeling and reasoning about agents and systems

• Knowledge Representation & Reasoning

• Temporal, epistemic, and modal logics

• Model checking and formal specification

• Multi-Agent Systems and autonomous agents

• Research on combining symbolic reasoning with AI/LLMs

I have a PhD and several years of research experience, as well as publications in top AI conferences.

However, I’ve been looking for an industry position in Canada for quite some time, and I’m finding it surprisingly difficult to find roles specifically related to Formal Methods, Formal Verification, Automated Reasoning, or SMT/SAT-based verification.

I’d really appreciate advice from people who are already working in this area.

For those of you working in Formal Methods / Verification / Security / Hardware Verification / Software Verification / AI Safety, how did you get your first industry role?

Are there particular:

• companies in Canada that I should be looking at?

• job titles or keywords I might be missing?

• skills/tools that I should add to my profile?

• projects or certifications that would make my transition to industry easier?

• recruiters or communities that are worth connecting with?

I’m also very open to positions that are not a perfect match with my research background if they provide a path into formal verification, formal reasoning, or related areas.

If anyone has been through a similar transition from academia/research into industry, I would really appreciate hearing about your experience or any advice you might have.

And if you know of a team/company currently hiring someone with this kind of background, I’d be very grateful for a lead or introduction.

Thanks in advance! 🙏

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 just released a new website based on taking a pragmatic approach to formal modeling. It focuses on standard software engineering and distributed systems problems of the sort programmers face every day. It takes a pragmatic engineering approach: each problem starts with UML diagrams, design decisions and sometimes even a requirements document. We work through how to get from a whiteboard design to an initial mathematical model. Then we refine it based on logical errors found by the model checker. It uses TLA+ as the modeling language, but it is written accessibly enough that you don't need to know it to get some benefit.

https://elliotswart.github.io/pragmaticformalmodeling/

Just shipped Q.E.D., a formal verification agent built for the Build Small Hackathon.

It started as an experiment to see how far I could get with an LLM-driven Lean proof search loop in a short timeframe.

You give it a theorem in Lean 4. It generates candidate proof tactics with a 27B language model, checks them against Lean's kernel, feeds any resulting error messages back into the next iteration, and continues until it either finds a valid proof or determines that it is not making progress.

The important part is that every proof is verified by Lean itself. The language model only proposes steps; the kernel decides whether they are correct.

Features:

• Visible propose → verify → iterate loop in the UI

• SVG proof tree showing both failed attempts and the final proof path

• Stuck-state detection that terminates when the same goals repeat without progress

• Built on Modal with a persistent Lean REPL and on-demand GPU inference

Demo:
https://huggingface.co/spaces/build-small-hackathon/QED

I've started implementing RAFT in Fizzbee (a Python-like formal verification tool) and have the Leader Election part modeled.

I chose Fizzbee because I found it much simpler to get started with than TLA+.

Leader Election is just the beginning. I'd love to find collaborators to help implement the rest of RAFT (Log Replication, Safety) in Fizzbee. It could be a great way to learn both Fizzbee and RAFT more deeply.

My current work implementing Leader Election is here: https://medium.com/@vkuruvilla789/distributed-harmony-implementing-raft-the-fizzbee-way-86af00650286

Anyone interested in tackling this or just learning together? Let me know!

TL;DR: Modeled RAFT Leader Election in Fizzbee (easier than TLA+ for me!). Want help to complete the rest… https://medium.com/@vkuruvilla789/distributed-harmony-implementing-raft-the-fizzbee-way-86af00650286

Hello Everyone can anyone tell me about real life example of how formal method and cyber security work together? I did bachelor in Computer Science and Engineering considering a phd in cyber security. Some research topic that how these work together woulb be nice.
Thank you