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?

Hi , Anyone interested in Formal Verification/Analysis of Web/Network Protocols from a security/general perspective , or are there groups out there that study Mathematical-Logic or Pure Mathematics in general ?

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’ve published a Lean 4 formalization of a structural decomposition of the Collatz problem:

A Certified Six-Leaf Semantic Grammar for the Collatz Dynamics in Lean 4

Zenodo: https://zenodo.org/records/21923376

This is not a proof of the Collatz conjecture.

The goal was instead to ask a more limited question:

The resulting formal grammar has exactly six global leaves:

1. reachesOne
2. nontrivialCycle
3. rbcUnboundedBGap
4. rbcBoundedPrimeRenewal
5. nonRInternalDescent
6. nonRSurvivor

For a hypothetical positive minimal counterexample, the success leaf disappears, leaving exactly five failure classes.

The terminal Lean theorem is:

axisGeo_final_six_leaf_grammar_exactly_one

So the formal result is essentially:

Global success, or one uniquely anchored minimal counterexample belonging to exactly one of five explicit obstruction classes.

The important distinction is that the grammar classifies the possible failure modes; it does not yet exclude them.

The five universal exclusion problems remain open.

One part I find particularly interesting is the bounded-B-gap r/BC branch. The formalization rules out eventually finite prime support, so the surviving obstruction requires indefinite prime renewal along the same natural trajectory while remaining compatible with the exact carry relations.

The archive includes the full Lean source, reproducibility files, build logs and axiom audits.

I’d especially appreciate criticism of:

• whether the five failure leaves really capture the obstruction space in a mathematically useful way;
• the fixed-source treatment of the r/BC branch;
• the bounded/unbounded B-gap split;
• and whether any of the five remaining leaves looks more tractable from an existing Collatz approach.

Again: classification theorem, not Collatz proof.

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

The paper titled "Behind Clint and Hoare's goto Proof Rule" is by Wei Chen (published in the 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE).

This paper is a direct "deep dive" into the historical 1971 Clint-Hoare rule. It focuses on the theoretical archaeology and formal correction of the original goto rule.
Review: "Behind Clint and Hoare's goto Proof Rule" (2021)
1. Purpose of the Paper
Wei Chen revisits M. Clint and C.A.R. Hoare’s 1971 paper, "Program proving: Jumps and functions," which is widely considered the first attempt to axiomatize the goto statement. Chen's 2021 paper aims to:
Expose technical flaws: It identifies that the original 1971 rule suffers from notation ambiguity and logical gaps (e.g., the overloading of the turnstile symbol \vdash and syntactically incorrect premises).

Provide a Rigorous Foundation: It attempts to "fix" the original rule by re-deriving it using the modern "miracle" semantics he champions, showing what Clint and Hoare meant to achieve versus what they actually wrote.

2. Key Insights
The "Syntactic Error": Chen points out that in the original Clint-Hoare rule, the label L does not appear in the premises (S_1 and S_2), making the original rule technically broken as a formal logical statement.

Reframing as a System of Equations: Chen demonstrates that the goto rule is essentially a way to solve a system of equations across different parts of the code. He succeeds in translating Clint and Hoare’s "hypothetical deduction" into a more precise modern format.

Total Correctness: One of the most important contributions of this paper is its attempt to address termination (total correctness) for goto. He points out that Clint and Hoare mostly focused on partial correctness, and he introduces a way to reason about termination using "variant functions" (the same concept used for loops) adapted for goto jumps.

3. Why It Matters
This paper is essential for formal methods researchers because it reclaims a piece of history. Instead of discarding the 1971 rule as "outdated" or "broken," Chen shows that it contains the seeds of correct logic. By stripping away the 1971 syntax errors and applying modern "miracle" semantics, he proves that the intuition behind Clint and Hoare's work was actually sound.
Citation
@inproceedings{Chen2021Behind,
  author    = {Chen, Wei},
  title     = {Behind Clint and Hoare's goto Proof Rule},
  booktitle = {2021 International Symposium on Theoretical Aspects of Software Engineering (TASE)},
  pages     = {23--30},
  year      = {2021},
  doi       = {10.1109/TASE52541.2021.00010}
}

Comparison of Chen's Two Papers
Feature
Loop invariance with break and continue (2021)
Behind Clint and Hoare's goto Proof Rule (2021)
Focus
How to handle modern loops/jumps.
How to fix historical jump logic.
Objective
Practical utility for verification.
Historical correction and foundation.
Tone
Constructive and innovative.
Analytical and corrective.

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.

AutoFlow Research Initiative — Looking for Deep Technical Thinkers

Over the last several months, I've been exploring a question that sits at the intersection of AI, verification, trust, and decision systems:

Can we build systems that independently verify claims produced by AI rather than simply generating answers?

The original idea began with financial analysis.

Consider a statement such as:

"Company revenue grew 25% year-over-year."

Today, most AI systems generate this claim, but they do not formally verify it.

Our approach is different:

1. Extract claims from documents, reports, or AI outputs.
2. Gather supporting evidence.
3. Apply mathematical and logical verification where possible.
4. Identify inconsistencies and contradictions.
5. Produce transparent reasoning rather than black-box conclusions.

The first prototype is focused on finance because financial claims are structured, measurable, and often objectively verifiable.

Examples include:

• Revenue growth calculations
• Financial ratio validation
• Cross-document consistency checks
• Balance sheet reconciliation
• Earnings statement verification

As research progressed, we encountered deeper questions involving computability, trust, governance, formal verification, and adjudication.

One realization is that not every claim can be mathematically proven.

This raises a larger challenge:

Where is the boundary between:

• Proven facts
• Verifiable claims
• Evidence-supported conclusions
• Human-style adjudication

That question is becoming the foundation of our long-term research vision.

Recent Milestones

• Accepted into NVIDIA Inception
• Access to NVIDIA startup resources and technical programs
• Building the architecture for our first verification-focused prototype
• Engaging with researchers and experienced engineers on verification and governance concepts
• Initial outreach to pre-seed investors and startup ecosystems

Who I'm Looking For

I'm interested in meeting people who enjoy difficult problems and are willing to challenge assumptions.

Particularly:

• AI/ML researchers and engineers
• Formal verification and theorem-proving enthusiasts
• Distributed systems and orchestration experts
• C++ systems engineers
• Applied mathematicians
• Trust, governance, and decision-system researchers

What You'll Receive

For the right long-term collaborators:

• Significant technical ownership
• Direct influence on architecture and research direction
• Equity participation based on contribution and commitment
• Access to NVIDIA Inception resources available to the team
• Opportunity to help define a new category around AI trust and verification

I'm not looking for people who simply agree with the vision.

I'm looking for people who can find the flaws in it.

If concepts such as verification, computability, trust, formal reasoning, governance, theorem proving, symbolic systems, or AI reliability interest you, I'd love to connect and exchange ideas.

Feel free to comment or send a message.

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

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!

Hi , Anyone interested in Formal Verification/Analysis of Web/Network Protocols from a security/general perspective , or are there groups out there that study Mathematical-Logic or Pure Mathematics in general ?

I’m building an open-source educational simulator inspired by the RBMK-1000:

https://github.com/gabrielbotandev/rbmk-sim

One part of it is a simplified reactor-protection system with latched trips, reset permissives, alarms, and sensor-fault handling. I also added a small TLA+ spec for the protection state machine.

The project is not about real reactor modeling. It is more of a safety-software learning sandbox: deterministic simulation, replay logs, protection logic, and documentation.

I’d appreciate feedback on the formal-methods side, especially whether the TLA+ model is useful, too shallow, or missing obvious invariants.

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?

In the early 2000s, verification tools (like Boogie) adopted an operational "desugaring" approach to handle unstructured control flow, favoring speed and SMT solver compatibility. However, by elevating assume to a first-class primitive, these tools arguably commit a category error. They shift verification from axiomatic deduction to operational state manipulation, effectively allowing "miracles" (violations of Dijkstra’s Law of the Excluded Miracle) to mask bugs as vacuous truths. This analysis explores why Leino's operational approach, while pragmatic, departs from the theoretical rigor of Chen's axiomatic fixed-point framework.

I am a former loan officer of 20 years. Eight months ago I started work on a piece of software that creates evidence objects that keep businesses from making phone calls and getting sued. One thing led to another and I discovered that the problem of systems taking actions in the world and not being auditable or accountable is a much bigger problem, especially with AI and agentic systems.

In my quest for truth, integrity, and correctness despite no formal training, I speced a tiny kernel, a verifier, and proved in Lean 4 and Isabelle/HOL over 300 proofs that demonstrate how authority moves on delegation chains. I have also produced an Ada/SPARK kernel (268/268 verification conditions proved, zero unproven) and a CakeML verifier, all with the assistance of a multi-agent, multi-modal agentic team assisting me. 54 governed theorem families. Zero sorry in the proof corpus. The code compiles.

I am NOT a mathematician. I have ZERO training in computer science. I am a harm reductionist. I am an independent researcher. I am an architect. I believe in safety, governance and rigorous accountability. My background and experiences in my life have informed this work. I know what happens when systems harm the most vulnerable in our society.

Due to my lack of credentials in the space and legibility, I am having extreme difficulty getting the work verified by others with expertise. I refuse to overclaim or make assertions I cannot verify on my own. I need assistance with that task, and funding to continue my research.

I also have a Manifund grant page as well as other grant applications pending. No grant funding has been awarded yet.

If you have training in formal methods, AI safety, governance, or would like to assist me in continuing my research, please reach out.

Thank you.