ANTHILL: a progressive formalization language for agent-supported software projects

R.S. Shevchenko, A.Yu. Doroshenko, O.A. Yatsenko

Abstract


The article presents the Anthill language — a specialized language for progressive (gradual) knowledge for malization, designed for use in real-world software projects with the integration of agent support, in particular large language models. Anthill allows you to describe, accumulate and maintain domain knowledge, functional and non-functional requirements, design solutions, invariants, integrity constraints and property proofs in a single structured knowledge base. A distinctive feature is that the knowledge base is stored directly in the pro ject repository file system, which ensures close versioned synchronization of specifications with code and fa cilitates their evolution throughout the development life cycle. The core of the language is made minimal and consists of only four basic constructs: namespace, sort, rule and operation. This architecture is similar to the core of modern automated theorem proving systems (e. g. Lean, Coq), where a small trusted core performs on ly the correctness check of the derivation, while the search for proofs, rule generation, specification refinement, and resolution of commitments are delegated to external agents. The main innovation of Anthill is the built-in support for partial (progressive) formalization: one and the same language allows for the description of knowledge across the entire spectrum — from free-text natural language comments in blocks through semi formal machine-verifying rules (Horn clauses) to fully formal proofs and laws of algebra. Three application examples are considered: structured task management, specification of communication protocols for embedded systems, and proof of properties at the compilation stage.

Problems in programming 2026; 1: 4-13

 


Keywords


formal specification; progressive formalization; knowledge base; stigmergy; multi-agent systems; large language models

References


L. de Moura, S. Ullrich, The Lean 4 theorem prover and rogramming language, in: 28th International Conference on Automated Deduction (CADE 2021), Lecture Notes in Computer Science 12699 (2021) 625–635.

The Coq Development Team. The Coq Proof Assistant. Accessed: 18.03.2026. https://coq.inria.fr

T. Nipkow, L. Paulson, M. Wenzel, Isabelle/HOL—a proof assistant for higher order logic, Springer, 2002.

J. Goguen, T. Winkler. Introducing OBJ. Technical Report, SRI International, 1988.

M. Clavel et al., Maude: specification and programming in rewriting logic, in: Theoretical Computer Science 285 (2002) 187–243.

L. de Moura, N. Bjørner, Z3: An Efficient SMT Solver, in: Ramakrishnan, C.R., Rehof, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008. Lecture Notes in Computer Science 4963 (2008) 337–340.

R.S. Shevchenko, A.Yu. Doroshenko, TermWare-3–term rewriting system, based on context-term calculus, Problems in programming 1 (2019) 48–58.

Anthill kernel language specification. Accessed: 18.03.2026. https://github.com/rssh/anthill

R.S. Shevchenko, A.Yu. Doroshenko, V.O. Lesyk, O.V. Savchuk, O.A. Yatsenko, Interface-oriented approach to modelling tools for multi-agent systems, Problems in programming 1 (2025) 110–117.

gRPC. Accessed: 18.03.2026. in URL: https://grpc.io/

Protocol Buffers. Accessed: 18.03.2026. https://protobuf.dev

R. Diaconescu, K. Futatsugi, CafeOBJ Report. World Scientific, 1998.

E. Meijer, Unleashing the power of end-user programmable AI, in: ACM Queue 23 (2025).

M. Odersky, Y. Zhao, Y. Xu, O. Bračevac, C.N. Pham, tracking capabilities for safer agents, in: arXiv:2603.00991 (2026) 1–21.

K. Yang, G. Poesia, J. He, W. Li, K. Lauter, S. Chaudhuri, D. Song, Formal mathematical reasoning: a new frontier in AI, in: arXiv:2412.16075 (2025), 1–42.

Google DeepMind. AI achieves silver-medal standard solving International Mathematical Olympiad problems (AlphaProof announcement). 2024.

P. Song et al., Lean Copilot: large language models as copilots for theorem proving in Lean, arXiv:2404.12534 (2024), 1–26.

X. Hu et al., APOLLO: automated LLM and Lean collaboration for advanced formal reasoning, arXiv:2505.05758 (2025) 1–28.

P. A. Abdulla, M. F. Atig, J. Cailler, C. Liang, P. Rümmer, When GNNs met a Word equations solver: learning to rank equations, in: arXiv:2506.23784 (2025).

R. Shevchenko, A. Doroshenko, O. Yatsenko, A. Nemish, Merging logic and the coinductive selection monad: mixing machine learning in to logical search, Communications in: ICTERI 2025. Computer and Information Science 2763 (2025) 33–46.


Refbacks

  • There are currently no refbacks.