goal: see how far llms plus gating and formalization can take us, starting with my own projects, and share what holds up.

reduce assumptions, never silently omit them — and know what's left.

also, check acceptance-format.

try it on your own system - clarify actual requirements and see if your system is compliant to the spec and that your tests properly verify things they should, i.e implementations is up to the requirements.

ideas, criticism, counterexamples and similar work are welcome: ivomatijasevic@gmail.com.

why does this page exist? because i want to share how i envision what software (in general artefact) production will be in 10 years, not bound by legacy limitations. also i would like to find people interested in same topics and results. especially if you have any more ideas, critcisms, counterexamples or similar work ( ivomatijasevic@gmail.com ).

missing element in building larger things without faults are the 3 pillars bellow. in short, formalization and grounding of logic, assumptions, defintions and protocols.

i do work here in my personal time as a personal project - i want to build a system that automates many aspects of my life but also would like to share findings with the world. other reason why i publicize most of it: to show the world i know what i'm talking about and direction of what im doing (most of the time). a short talk or mail correspondance doesnt show much and i am not involed in academia.... so best way is to show and produce something useful to the world in open format.

my view is that llms change the economics. writing verifiable code and actually verifying it becomes cheap at scale.

i would say the future has 3 paths for software:

• legacy code and apps — not optimized for llm autonomy
• "disposable code" — an llm-produced app for a use case
• "correct code" — not just unit-tested code: code derived from a spec, shipped with proofs for the relevant characteristics

what does this mean:

• we need good & fast & llm-friendly model checkers for the relevant languages (my assumption is rust will be most relevant in the future, so i choose to rely on kani and aeneas for now)

• the most critical parts of the core of a system need to be:

  • CORRECT — satisfies the SPEC on every input, covered by proofs and tests

  • SOUND — no panics, no undefined behavior, no silent corruption

  • SECURE — the properties that protect users hold by construction, not by testing effort

two active repos i have:

• rs-verified-der - work in progress, a partially formally verified DER encoder/decoder (most proofs are bounded; selected properties are proven in lean for inputs of any length), more of a showcase rather than a library i expect to replace exising solutions. but i do plan to use it for my internal systems.

  question i try to answer: how do i show you that this DER encoder/decoder is good?

  answer is i try to do it via acceptance.

  • acceptance manifest — claims, evidence and grades

  • proof manifest — proven properties, bounds and assumptions

  • coverage — which X.690 rules are covered, and how

  • replay — re-run the evidence yourself

  • autoprover-core — lean proofs, an automated proving pipeline architecture, and a runnable reference implementation used in automating formal verication work but also as core of the crystal mentioned below.

also, have few kani upstream contributions since it pairs well with the project. i also back kani, since my work relies on it.

we need an easy way to ship code (or really any artefact in the world where most artefacts are partially or fully AI generateed) together with its spec and its evidence: proofs, tests, reviews (per authority) and also evidence of proofs, thest runs and signs of review of the authority.

an artefact should come with what its consumer needs to accept it, not just the artefact itself. the acceptance format is one such format: a contract between the producer and the consumer (who may be the same person/organization) on what was produced, how well it was checked, and with what evidence, so the consumer can check it.

two things that are most important:

• a claim gets more weight only when its test or proof is shown to FAIL on a broken version. a check that cannot fail proves nothing. it requires mutation in code and rerun of test. manually its cumbersome but llm can do it or -- better yet, automate it in code :)
• what was NOT VERIFIED is written down too. if something is too hard to check, the record says IT WAS NOT CHECKED rather than leave it assumed. i use it like that in my own systems, so i know it is useful. many things will stay hidden assumptions, we are all limtied and its hard to enumerate every assumption or requirement but we simply expand them as we find them or get better models which will find more of them.

the format checks the records -- it does not certify the software. really it enumerates the requirements in a good way.

• acceptance-format — the format (claims and their evidence) and the protocol (consumer's spec → producer's package → consumer's decision). version 0.4.0, locked, not ratified. apache-2.0 or mit. artifact agnostic, so its not only for rust code but any artifact that can be grounded by an oracle.
• acceptance as a protocol for delegated work — the paper behind the format (preprint).
• accepted-work — record formats around an acceptance decision: obligation, relation, trigger, impact rule, fill contract. early development, not in use yet. apache-2.0 or mit.

llms make it easy to check code against the spec, but the hard part then is: what should the spec say.

this still stays critically people endeavour due to intent agreement.

thats why we firstly focused doing acceptance examples on well defined RFCs - but even then they may be ambiguous.

strictest specifications become the easiest in world of LLMs since intent drift is much smaller there.

intent projection is one of most important items that i focus on -- but no public works on it (yet).

examples of acceptance for existing RFCs and standards (still this is just our interpretation of it) - note list below is autocurrated:

• acceptance-examples — requirement lists, one row per requirement: JOSE/JWT, X.690 DER and others.
• first acceptance manifests — the lists applied to go-jose, tink-py and Go's encoding/asn1. only findings already reported to the maintainers; no conformance claimed.
• X.690 DER requirement list — the DER list used by rs-verified-der (pinned commit).

applying the lists found some irregularities in code and missing test cases in public repositories.

• acceptance roadmap — next versions of the format
• more acceptance manifests, one per library, in acceptance-examples
• requirement lists as trees: a row can split into child rows (today the lists are flat)
• DER verification map — what is proven, and what is planned next

every system rests on assumptions. the dangerous ones are the hidden ones — trust taken without ever being named.

our way of work: either a statement is proven correct from other statements and/or assumptions OR it is stated as assumed.

one obvious place where we assume correctness without explicitly stating it: we trust 3rd party libs, tools, compilers, hw, etc. with llms we should make these assumptions loud... also acceptance format is created exactly for that.

one of only handwritten texts in the repos i own is this one -- rest are LLM produced but mostly reviewed/adapted (the relevant ones where intent is critical. where things are mechanical i mostly do not review). priority is that repos do not overstate their results and claims while also not losing the history and all important data (and rules for llm workers).

i started with the idea of 'foundry' and the underlying 'crystal' - just my illustrative way to describe it.

what it is - an artefact producing engine with spaces for LLMs and people both but mostly mechanized - really consider an automatic code producing machine. LLMs can do this today, i understand but there is no guarantee the code is correct. main point of foundry is the gating and validation become critical elements of the artefact itself.

and crystal - its a corpus of lean proofs underlying the foundry GROUNDING it in assumptions and axioms.

autoprover core is really a crystal core.

foundry is not one program: its an idea which can be adapted.

consider producing game software and control software for airplane. you cannot model a producing engine in same way: one accepts bugs as normal - fix can be done in next release - but if other one has a bug, well not good.

so foundry can have different assumptions and definitions but - the core - is invariant.

model of such foundry is in the crystal - deepest grounding possible.

variant theorems are also to be added to the crystal as need grows but really every foundry build is better built to a larger crystal which grows.

ive built 4 iterations of foundry and i postponed the work on 5th - too large of a project and started way too early. what i DO REALLY NOW -- is elements NEEDED for the foundry, ie protocls are the nervous system, used to build coded elemeents, so most items are MECHANICAL (code) with LLMs only in places where we need semantic openeness or coding is too expensive.

every pillar mentioned above is really a pillar of the foundry... those builds are private and not really worthy sharing.

as mentioned, i now focus on 3 pillars that first need to be well developed before i consider reopening the full foundry implementation.

i do activley work on implementing all 3 pillars in my own systems, kind of simple protofoundry, directly applying mechanization to my subsystems, one item at a time.

building from bottom up rather from top down.

of course none of the steps here are easy or really manageable by one person but i think steps are feasible and necessary longterm for llm-generated code in serious enough systems.

autonomous artefact-producing-systems still need to be easily auditable, person-overridable and safe -- that's the point of "shift left" move: reduce problem-source surfaces to specs and mechanize most elements so no hidden non-wanted intent leaks into produced artefacts (in general, we talk about code, i.e commit or an application as primary example of a produced artefact).

i looked for existing papers on the subject and 'did not find the same synthesis or threshold formulation', to be more precise, so i prepared few preprints.

then it grew and now its really a precrystallized foundry theory in preprint-form.

it kind of helps with organization of theory but also allows easier sharing. list below is autocurated:

1. A Fault-Tolerance Threshold for Gated Agentic Computation: Reliable Long-Horizon Work from Unreliable Executors — Models work as segments checked by imperfect gates. Under stated assumptions, more gates can extend reliable work, but shared blind spots limit that extension.
2. Generated Gates Inherit Their Generator's Blind Spots: A Diversity Floor for Self-Generated Verification — Models why checks generated within one model family retain that family's blind spots. Reducing this limit requires a source that can distinguish faults the family cannot.
3. Escape, Cost, and Correlation at the Verification Floor of Gated Agentic Computation — Studies how faults that pass verification affect larger outputs. It also compares verification costs and examines faults that share a source.
4. Progressive Semantic Mechanization: Compiling Intellectual Work into Deterministic Programs with Typed Semantic Holes — Models work as a program with typed gaps for model or human calls. It studies when acceptance checks can support moving that work to deterministic programs.
5. Beyond Constant Fault Rates: Reliability Bounds for Gated Computation and Semantic Mechanization — Examines which earlier reliability results hold when fault rates change, work segments depend on each other, or retries retain defects. It separates results that still hold from formulas that need replacement.
6. Risk-Gated Mechanization: Severity, Verifiability, and Decisions Invariant to the Executor's Error Law — Adds fault severity and a risk budget to decisions about replacing work with deterministic programs. It gives conditions under which that replacement is required, allowed, or forbidden.
7. Allocation and Coordination under Scarce Resources: Admissible Routing, Prices, Review Sets, and Containment for Gated Work — Studies how to share limited resources among work options that meet their safety conditions. It distinguishes resource allocation from executable schedules and examines the value of reviews.
8. Acceptance as a Protocol for Delegated Work: Claims, Failure Witnesses and Refusal — Describes a consumer's specification, a producer's claims and evidence, and a recorded acceptance decision. Claims receive weight only with a recorded failure witness and a command that can be run again; gaps remain visible.

simulations: gated-computation-sim.

i consider llms necessary but kind of like mitochnordria is for cell. yes, you would not have complex mulicellular organisms without it but still its not the main target. its a neccessray ingreedeint (not ideal comparison but - just for scale of multiceluar organism and systems i woudl say llms could build)

another comparisson id to use: llms used today are like 18th century clerks, they do everything manually, or maybe build themselves some useful tools. to get "nonviby" output we need to first gate but maybe more importantly formalize the way work output is combined into larger outputs.

i think the future needs more mathematicians, not fewer. machines will increasingly produce the proofs... but - what i consider at least, mathematics is the science (or if you want to be more strict, investigation) of structures: every possible combination of definitions, axioms and logics (what does this not cover? --it does not cover meassurments, the measurement part is the science. rest is math imho). point is people with math bacground are good with formalizations and generalizations and this is something really missing in the vibed world.

• masters in math and CS
• 10+ years in Erlang systems

pretty readme — claude's neutral view of the system, written from this page and the public repos.