In two years, proof assistants went from specialist tools to front-page news. At the Agda Implementors' Meeting we presented "Formal Verification in the Al Era: The Moment Proof Went Mainstream". FormalFoundry.ai has been building in this space since 2023. At the time, that was a niche position. Today it's where the field is heading. The talk drew on dozens of conversations we've had along the way with industry leaders, engineers, policymakers and defence and security representatives. Our clearest lesson: everyone wants Al or software they can trust, but few yet know that trust can be proven rather than estimated. As Al writes more of the world's code and decisions, that difference stops being academic. It becomes the basis of trust. That's what we build.

AI-scale formal verification is no longer a research bet. FormalFoundry.ai has been building in this direction since our 2025 whitepaper: language models generate candidates, proof assistants decide what holds. The model accelerates. The checker is the boundary of trust. What building this in Cubical Agda has taught us: → Scale comes from reusable checked infrastructure, not one-off proofs. Our libraries cover JSON, typed HTML/CSS, IEEE-754 floating point and constructive real analysis (TYPES 2026). → The hardest part is rarely the proof. It is the specification: turning messy domain text into a statement worth proving. → Code is only one surface. The same pipeline (domain text → formal specification → prover check → audit artifact) applies to legal obligations, tax rules, clinical safety constraints and autonomous system protocols. That last point is our focus. Software verification asks: does the code match the spec? We also ask: is the spec faithful to the rules it claims to implement? Codex Scribe, which we premiered at @Milipol_Paris is built for exactly that step. Proof at scale is arriving for software. Rulebooks are next.

Agda Implementors' Meeting XLIII is underway at the Podkarpackie Center for Innovation in Rzeszów! We are proud to sponsor this gathering advancing dependently typed programming, formalization, and the future of the Agda proof assistant. Thank you to the organizers, our hosts at PCI, and everyone taking part.

We went to CSF'26 to listen first. A few unscripted conversations with senior decision-makers from banking and medtech told us more than any market report could. We wanted to deeply understand the real constraints these teams face as they deploy AI in highly regulated, high-responsibility sectors. Many of them were surprised to learn that we are building sovereign capabilities in formal verification right here in Poland to tackle these exact AI safety and compliance challenges. We're leaving with clear conviction - the direction holds. In fact, several of these discussions are already moving forward into a technical dialogue phase, marking the next concrete step for FormalFoundry.ai.

"From Word Statistics to Artificial Intelligence" - that was the title of the lecture we gave this week at the Faculty of Economics and Finance, University of Rzeszow. The talk traced the path from early work on semantics and the structure of language - decades of linguistic research that quietly laid the groundwork for today's breakthroughs - to how modern language models actually work, and what the distinction between "fast" and "slow" thinking means for how AI systems make decisions. The room held faculty, researchers, and the economists, analysts, and managers of tomorrow - people who, for the most part, won't build the next generation of AI, but will work with what it produces. And the AI they'll encounter is already evolving past today's LLMs: neuro-symbolic systems and formally verified models, where statistical inference is paired with mathematical guarantees about behavior. That's the frontier we are building on.

At the URAI Summit panel the discussion centered on how AI translates into real competitive advantage. FormalFoundry was represented by our co-founder Grzegorz Kunicki. The bottleneck isn't model capability - it's the ability to give experts a structure that scales their judgment to the volume of decisions modern organizations face every day. Not to replace them, not to extract their knowledge, but to let one expert's reasoning operate reliably across thousands of cases that would otherwise never reach their desk. In finance, compliance, critical infrastructure, "the model said so" isn't good enough - the logic has to be verifiable. That's the gap our work is built to close. Artur Pieczonka (@Deloitte Central Europe BSC) framed the enterprise side - how leadership roles must evolve in data-driven organizations, and why successful AI adoption depends less on tool deployment and more on the deeper adaptation of decision-making processes. Worth continuing that conversation. Grateful also to dr Grzegorz Hajduk (University of Rzeszów) on preparing graduates for hybrid intelligence, Paweł Wais (Marshal's Office of Podkarpackie) and Jarosław Reczek (PSG) on the regional ecosystem making this transition possible. Special thanks to Professor Bogdan Wierzbiński, Dean of the Faculty, for bringing together a discussion that engaged academia, enterprise, public administration, and deep-tech around a question that genuinely matters.

SPRIND brought its Frontier AI roadshow to Warsaw. We joined the discussion on how Europe should think about AI and the infrastructure needed around it. At FormalFoundry.ai, our focus is formalization. Frontier models are becoming increasingly capable heuristic systems. But to use AI in domains where correctness matters, models need to connect with precise representations of the world they operate in: regulations, procedures, contracts, technical protocols, engineering constraints, and institutional knowledge. That is the bottleneck we work on. Before proof assistants and formal methods can become useful across the AI ecosystem, real-world domains need to be translated into structures that machines can check, reason over, and verify against. Our work is to build products and services that support this process: helping organizations turn complex domain knowledge into formal specifications, proof-ready representations, and foundations for neurosymbolic AI systems. What we were in Warsaw to explore is the next chapter - scaling what we already do into a fully independent European neurosymbolic AI lab, where pairing heuristic power with formal rigor is the default, not a research curiosity. Europe is uniquely positioned to host that kind of lab, and we think the moment to build it is now.

SpaceShield Summit 2026: Grzegorz Kunicki moderated and participated in the "Technological Sovereignty of Poland in the AI Era" panel alongside Ewa Dolińska-Wysocka (@bielikllm ) and Michał Kwiatkowski (@AldecInc). On the second day of the event, we presented our recent R&D progress and showcased CodexScribe. This tool advances our mission to bridge the gap between intuitive natural language and formal specifications, facilitating the iterative refinement of safety-critical logic. We are moving beyond creative heuristics toward "Formalized Reasoning" where AI outputs are verified against rigorous domain logic to ensure outcomes are provably correct.

As AI continues to redefine the landscape of defense and space, the question of autonomy has never been more critical. We are proud to announce that our Co-founder, Grzegorz Kunicki, will be joining the panel "Poland’s Technological Sovereignty in the Era of AI" at SpaceShield Summit 2026! 🛡️🚀 The discussion will dive deep into how strategic innovation and local AI capabilities are essential for national security and resilience in a dual-use world. 📅 March 3-4, 2026📍 Stalowa Wola, Poland We look forward to connecting with leaders across the defense, space, and deep tech sectors to discuss the future of secure, sovereign technology. See you there! 🤝

AI is making formal verification scalable. As Martin Kleppmann notes, proofs are no longer the bottleneck - specifications are. At FormalFoundry, we help translate expert knowledge into precise logic. Formalize your business rules without a PhD. Ask us about our pilot programs 🚀 martin.kleppmann.com/2025/12…

Great sessions with the MBA students at @UR_Rzeszow, led by our COO. By illustrating the friction between probabilistic models and the need for deterministic guarantees, he highlighted the danger of scaling stochastic intuition without the safety net of formal logic. Organizations that ignore this gap risk automating errors at an unprecedented scale - undermining the very efficiency they set out to achieve. We believe in educating leaders who understand that true innovation requires the immense potential of agentic workflows, backed by formal logic and verifiable safety.

We won the @Milipol_Paris Innovation Award 2025 in Cybersecurity & AI. This sends a clear signal from the world’s leading homeland security stage that #neurosymbolic AI is a promising direction for delivering safe and explainable AI in the field. While others debate “Prompt Engineering,” we use “Logic Engineering.” We bring mathematical and logical precision to domains where failure is not an option: compliance, national security, infrastructure and autonomous systems. During our talks in Paris with defence officials and equipment manufacturers, the consensus was clear: black-box AI has hit its breaking point. The demand for transparent, auditable logic has become the industry’s priority.

Artificial intelligence is now one of the strongest forces shaping the modern world. At the upcoming “Technology, Economy and Ecology – Three Forces Shaping the World” national conference, organised by the Institute for Security and International Development (@InstytutBiRM), Grzegorz Kunicki, COO of Formal Foundry, will speak about why trust has become the new currency of technological progress. Talk title: “The limits of trust in technology in an era of AI-driven change. When system decisions become opaque - how to regain control.” His presentation will explore how world modeling, formalization and formal verification can restore clarity, accountability and control in AI-driven environments. @InstytutBiRM is a research-driven think tank engaging with economic, geopolitical and security challenges. Its mission is to deepen public understanding of the forces shaping global stability and development.

Beam engines started the revolution; thermodynamics and precision engineering scaled it. LLMs will kick off a lot, but scaling long-agentic workflows needs formalized domains + a precise, machine-checkable proof assistant alongside the model. DM us to set up a call to see the demo.

California’s SB-53 calls for transparency frameworks describing how AI developers apply standards and best practices. At FormalFoundry, we explore ways to translate such frameworks into formal, machine-readable specifications - so compliance can be proven, not just declared in a PDF. Our aim is to make “trust but verify” an engineering property, not a policy slogan.