Using the JSON Server

Using the JSON Server

AProVE can run as a line-delimited JSON (NDJSON) daemon. It reads one JSON request per line from stdin and writes one JSON response per line to stdout. Logs go to stderr and never contaminate the JSON stream.

This is useful for integrating AProVE into scripts, batch tools, or external processes without paying the JVM startup cost on every invocation.

Starting the Server

Build the dist JAR, then launch directly:

ant -f build-aprove.xml dist
java -cp "dist/lib/aprove.jar:lib/*:res-classes" -Djava.library.path=lib aprove.api.server.AProVEServer

From VSCode: use the AProVE (Server) run configuration (rebuilds automatically before starting).

The server runs until stdin is closed (EOF). Send requests one per line.

Request Format

Each line is a JSON object with the following fields:

Field	Type	Required	Description
file	string	yes	Absolute or relative path to the problem file (.ari, .trs, etc.)
timeout	number (ms)	no	Analysis timeout in milliseconds. Default: 60000
name	string	no	Display name for the problem. Default: filename
rewriteStrategy	string	no	"innermost", "outermost", or "full"
goal	string	no	Override the goal declared in the file. Accepted values: "ast", "sast", "termination", "complexity", "confluence", "infeasibility", "past" (case-insensitive)
cert	boolean	no	If true, produce a CPF3 certificate. Default: false

Example request:

{"file": "/path/to/problem.ari", "timeout": 30000, "rewriteStrategy": "innermost"}

Example request with certification:

{"file": "/path/to/problem.ari", "timeout": 30000, "cert": true}

Response Format

Each response is a JSON object on a single line:

Field	Type	Description
name	string	Problem display name
result	string	"YES", "NO", or "MAYBE"
time	number	Elapsed time in milliseconds
timeout	boolean	true if the analysis timed out
error	string or null	Error message if something went wrong, otherwise null
cpf	string or null	CPF3 certificate XML (only present when cert: true and result is YES or NO; null otherwise)
proofTree	array	List of proof tree nodes (see below)

When cert: true is sent, the server restricts itself to certifiable proof techniques and produces a CPF3 certificate via the cpfconverter tool (configured via the CPF_CONVERTER environment variable, default /opt/bundle/cpfconverter/cpf2_to_3.sh). If the result is MAYBE, or certification fails for any reason, cpf is null.

On a parse error or unexpected exception, a minimal error response is returned:

{"result": "ERROR", "error": "description of the error"}

Proof Tree Nodes

The proofTree array contains one entry per node in the proof tree, in the order they were created. Each node is a JSON object:

Field	Type	Description
index	number	Zero-based index of this node
parentIndex	number or null	Index of the parent node (null for the root)
obligationName	string	Name of the proof obligation at this node
obligationPlain	string	Plain-text representation of the obligation
processorName	string or null	Name of the processor that produced this node (null for root/unprocessed)
implication	string or null	Plain-text implication string from the proof step
proof	string or null	Full plain-text proof detail for this step

The root node has parentIndex: null and processorName: null. Leaf nodes that were not processed (e.g. obligations discharged by a parent) also have null processor fields.

Sending Requests from the Command Line

Single request (pipe to the server):

echo '{"file":"/path/to/problem.ari","timeout":30000}' | java -cp "dist/lib/aprove.jar:lib/*:res-classes" -Djava.library.path=lib aprove.api.server.AProVEServer

Batch processing (one JSON request per line, one JSON response per line):

java -cp "dist/lib/aprove.jar:lib/*:res-classes" -Djava.library.path=lib aprove.api.server.AProVEServer < requests.ndjson > results.ndjson

For interactive use, start the server and type requests — a response is written after each line.

Notes

• Requests are processed sequentially — the server handles one at a time.
• The server does not restart between requests; AProVE's internal state is reused across calls in the same process.
• If the file path does not exist or is unreadable, the response will have "result": "ERROR".
• rewriteStrategy and goal are passed directly to AProVE's CLI override mechanism and are only meaningful for .ari files. Not all goal/strategy combinations are valid for every problem type; unsupported combinations typically produce "MAYBE".
• cert: true requires the cpfconverter script to be available. Set the CPF_CONVERTER environment variable to its path if it is not at the default location (/opt/bundle/cpfconverter/cpf2_to_3.sh).