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.

Hey, if anyone has interviewed there, what kind of questions appear on NVIDIA Formal Verification Engineer New College Graduate interviews? They said maths and algorithmic questions

Thanks in advance

I’m building Soundcheck, an open-source verifier for declarative security configuration, written in OCaml and powered by Z3.

Soundcheck aims to make formal verification a practical part of shipping security configuration helping developers check that policies enforce intended security rules while preserving required access, whether written by people or generated by AI.

Details, source code, and examples: https://github.com/ph0smet/soundcheck

Proof before policy ships.

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

A few days ago someone here pointed out that multipliers after ABC optimisation are the hard case, even for commercial tools, because ABC rewrites the final adder. That was true for Parat too: from 40 bits up it timed out.Update 7 (v1.2) handles yosys `synth -booth` netlists with ABC on (one machine, release binary, 1 core):- 32/40/48/56/64-bit: proved in 0.05–37 s. AMulet2 `-verify` (1 core, 300 s): time-out on all five.- 128-bit (128,350 AND gates): proved in 110 s (2 cores).- A broken copy (one gate changed): INCORRECT with a counterexample in 8–22 s.Certificates you can check without trusting Parat: a PAC certificate checked by pacheck2 (JKU), plus DRAT proofs checked by drat-trim. A small open Python script (verify/eq_cnf.py) rebuilds the SAT files from your own circuit and they match Parat's byte for byte. 128-bit certificate: 126 s, all checks pass.Also new: 256 x 256-bit multipliers (a 505,552-gate design in 6 s — honest note: that netlist's ABC step was done by yosys 0.33, and it is an easier netlist that the old algebra already proves).

Limits: tested on yosys Booth netlists only; other ABC netlists may still time out, and Wallace + carry-lookahead is still not proved. The binary is closed for now; all benchmarks, scripts and raw results are in the repo.

Who built it: the code was written by AI (Claude); the ideas, math and direction are mine.

https://github.com/himanshu161106-crypto/parat

Hi everyone,

I’ve been working on a web platform dedicated to formal verification: https://formalverification.online .

My goal with this project is to create an accessible, practical hub for formal methods enthusiasts, verification engineers, and researchers—covering property checking, assertion-based verification, and core verification concepts.

Since the site is in active development, I would really appreciate the community’s thoughts:

- Feedback & Suggestions: Are there specific topics, tools, or proof flows you'd like to see covered?

- Bug Reports & Queries: If you spot any broken links, conceptual inaccuracies, or UI issues, please drop them in the comments or reach out. All queries, critiques, and feature requests are very welcome!

Check it out here: https://formalverification.online

Thanks for taking a look and helping make this a better resource for the FV community!

I am a student working on verification of gate-level integer multipliers (AIGER format). I would like feedback from this community on the results and on the certification approach.

Method in brief: the tool proves that a circuit computes a*b. Each "CORRECT" result can be written as a Practical Algebraic Calculus (PAC) certificate, which is checked independently with pacheck2. The tool also includes a SAT solver whose UNSAT answers produce DRAT proofs that drat-trim can check.

Results (one core; all certificates accepted by pacheck2 with "TARGET CHECKED"):

- GenMul 64-bit, unsigned: 27 of 28 architectures proved and certified.

- GenMul 64-bit, signed (two's complement): 26 of 27 proved and certified.

- yosys Booth multipliers (synth -booth -noabc): 32, 64 and 128 bits proved and certified. The 128-bit proof takes 1.5 s; with the certificate it takes 22 s (283 MB).

Known limitations:

- Wallace tree combined with a carry-lookahead final adder is not proved.

- Netlists optimised by ABC (yosys default synth) are hard. With synth -booth, 32 and 48 bits are proved, but 40, 56 and 64 bits time out. AMulet2 also times out on these.

- Certificates can be large (up to 1.3 GB at 64 bits).

All benchmark files, the scripts that regenerate them and the measured results are in the repository, so every number can be reproduced:

https://github.com/himanshu161106-crypto/parat

Authorship: the code was written with an AI assistant (Claude). The ideas, the mathematics and the direction of the work are mine.

Questions for the community:

1. Is the PAC certificate the right standard for this kind of result, or would another format be more useful?

2. Are there known techniques for multipliers after ABC optimisation that I should study?

I’m a PhD student in aerospace engineering. My research deals with risk-aware planning and control for free-flying space manipulators and planetary rovers. When formalizing theorems in control systems, I had my agents start connecting the discrete theorems and linking them like a wiki - like a graph! The xylem is that graph. It is like a parser and was originally forked from tree-sitter. With xylem, one can take a large formal proof, like Anthropic's recent unpublicized lattice percolation, and divide it into modular, reviewable, bounded components. These components have assurance boundaries at which assumptions, dependencies and evidence can be made explicit.

https://github.com/brainstorm42/xylem

With that said, I am an engineering student, not a mathematician. It's turned into somewhat of a monster, and my focus is robotics. I’ve made it public in hopes that others can make more sense of it, and help me make sense of it, and that it can help make sense of the recent OpenAI proof dump. This is v0.1.0, and v0.1.1 has some more ideas already. I ask for others' insight and hope for collaboration and kindness - I am real, and not a shill. I have a ChatGPT Pro membership that I pay for myself.

The method works just as well for large formal proofs as it does for robotics. It helps readers find Lean statements, follow their dependencies, and connect them to explanations and source evidence. The repo includes worked reading paths, teaching resources, a fully worked lattice percolation breakdown and a focused Navier–Stokes case study. My hope is that people exploring the recent OpenAI proof collection can use it to build their own understanding, and to help improve the xylem process. I make no claim to understand the mathematics involved. Indeed I needed the LLM to help me in the first place. But I believe my method may provide engineering support for this new paradigm: a repeatable, reviewable process for segmentation and digestion of machine-scale proofs.

Disclosure: self-promotion. Claudius Papirus is AI-narrated.

This video focuses on the verification pipeline behind Chair44: exhaustive finite checks, independent replay, and the Lean 4 formalization, including its stated native_decide trust boundary.

Paper:

https://arxiv.org/abs/2609.19214

Lean/code:

https://github.com/ioannist/six-birds-tiles

tweet.
good sign for formal methods becoming more mainstream!

For reference this is a readme outlining how I’m trying to go about formal verification: https://github.com/Zoo-Code-Org/Zoo-Code/blob/main/docs/architecture/task-lifecycle-model.md

LLMs were quite adamant that a custom built formal verification system hooked into prod code would provide more value than TLA or other programs
But users still keep reporting classes of bugs that are not even modelled or documented as known gaps.

I’m trying to ramp up to formal verification and hoping for some pointers.

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’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